equal
deleted
inserted
replaced
93 |
93 |
94 lemmas L_nat = Ord_in_L [OF Ord_nat] |
94 lemmas L_nat = Ord_in_L [OF Ord_nat] |
95 |
95 |
96 theorem M_trivial_L: "PROP M_trivial(L)" |
96 theorem M_trivial_L: "PROP M_trivial(L)" |
97 apply (rule M_trivial.intro) |
97 apply (rule M_trivial.intro) |
98 apply (erule (1) transL) |
98 apply (erule (1) transL) |
99 apply (rule nonempty) |
|
100 apply (rule upair_ax) |
99 apply (rule upair_ax) |
101 apply (rule Union_ax) |
100 apply (rule Union_ax) |
102 apply (rule power_ax) |
101 apply (rule power_ax) |
103 apply (rule replacement) |
102 apply (rule replacement) |
104 apply (rule L_nat) |
103 apply (rule L_nat) |