begin
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
Lm1:
1 = succ {}
;
theorem Th17:
theorem
theorem Th19:
theorem
theorem
theorem Th22:
theorem
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem
theorem
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem
canceled;
theorem
for
A,
B being
Ordinal st
A *^ B = 1 holds
(
A = 1 &
B = 1 )
theorem Th42:
:: deftheorem ORDINAL3:def 1 :
canceled;
:: deftheorem Def2 defines +^ ORDINAL3:def 2 :
:: deftheorem defines +^ ORDINAL3:def 3 :
:: deftheorem defines *^ ORDINAL3:def 4 :
:: deftheorem Def5 defines *^ ORDINAL3:def 5 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
for
A,
C1,
D1,
C2,
D2 being
Ordinal st
(C1 *^ A) +^ D1 = (C2 *^ A) +^ D2 &
D1 in A &
D2 in A holds
(
C1 = C2 &
D1 = D2 )
theorem Th57:
theorem
:: deftheorem Def6 defines -^ ORDINAL3:def 6 :
for
A,
B,
b3 being
Ordinal holds
( (
B c= A implies (
b3 = A -^ B iff
A = B +^ b3 ) ) & ( not
B c= A implies (
b3 = A -^ B iff
b3 = {} ) ) );
:: deftheorem Def7 defines div^ ORDINAL3:def 7 :
:: deftheorem defines mod^ ORDINAL3:def 8 :
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th65:
theorem Th66:
theorem Th67:
theorem
theorem Th69:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th77:
theorem Th78:
theorem
theorem
theorem Th81:
theorem
theorem
theorem
begin
theorem
theorem
theorem Th87:
theorem