changeset 13628 | 87482b5e3f2e |
parent 13566 | 52a419210d5c |
child 13634 | 99a593b49b04 |
--- a/src/ZF/Constructible/L_axioms.thy Fri Oct 04 15:23:58 2002 +0200 +++ b/src/ZF/Constructible/L_axioms.thy Fri Oct 04 15:57:32 2002 +0200 @@ -95,8 +95,7 @@ theorem M_trivial_L: "PROP M_trivial(L)" apply (rule M_trivial.intro) - apply (erule (1) transL) - apply (rule nonempty) + apply (erule (1) transL) apply (rule upair_ax) apply (rule Union_ax) apply (rule power_ax)