begin
theorem Th1:
theorem Th2:
theorem
theorem
theorem Th5:
:: deftheorem defines last ORDINAL2:def 1 :
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem Th10:
theorem Th11:
theorem
canceled;
theorem
theorem
theorem
theorem
canceled;
theorem Th17:
:: deftheorem ORDINAL2:def 2 :
canceled;
:: deftheorem ORDINAL2:def 3 :
canceled;
:: deftheorem ORDINAL2:def 4 :
canceled;
:: deftheorem ORDINAL2:def 5 :
canceled;
:: deftheorem defines inf ORDINAL2:def 6 :
:: deftheorem Def7 defines sup ORDINAL2:def 7 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem Th26:
theorem Th27:
theorem Th28:
theorem
theorem
theorem
theorem
:: deftheorem Def8 defines Ordinal-yielding ORDINAL2:def 8 :
theorem
canceled;
theorem Th34:
:: deftheorem defines sup ORDINAL2:def 9 :
:: deftheorem defines inf ORDINAL2:def 10 :
theorem
:: deftheorem defines lim_sup ORDINAL2:def 11 :
:: deftheorem defines lim_inf ORDINAL2:def 12 :
:: deftheorem Def13 defines is_limes_of ORDINAL2:def 13 :
:: deftheorem Def14 defines lim ORDINAL2:def 14 :
:: deftheorem defines lim ORDINAL2:def 15 :
:: deftheorem defines increasing ORDINAL2:def 16 :
:: deftheorem defines continuous ORDINAL2:def 17 :
:: deftheorem Def18 defines +^ ORDINAL2:def 18 :
:: deftheorem Def19 defines *^ ORDINAL2:def 19 :
:: deftheorem Def20 defines exp ORDINAL2:def 20 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
Lm1:
1 = succ {}
;
theorem
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem
theorem
theorem Th60:
theorem Th61:
theorem Th62:
theorem
theorem
canceled;
theorem
:: deftheorem defines is_cofinal_with ORDINAL2:def 21 :
theorem Th66:
theorem
theorem