Theorem _nf_true ≪ | index | src | ≫

\nf\true（不可引用）

theorem _nf_true {x: set}: $ \nf x \true $;

Step	Hyp	Ref	Expression
1		true_proof	\true
2	1	_nf_prov	\nf x \true

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4, ax_10)