begin
theorem
canceled;
theorem
canceled;
theorem Th3:
for
X,
Y,
Z being
set holds
( not
X in Y or not
Y in Z or not
Z in X )
theorem
for
X1,
X2,
X3,
X4 being
set holds
( not
X1 in X2 or not
X2 in X3 or not
X3 in X4 or not
X4 in X1 )
theorem
for
X1,
X2,
X3,
X4,
X5 being
set holds
( not
X1 in X2 or not
X2 in X3 or not
X3 in X4 or not
X4 in X5 or not
X5 in X1 )
theorem
for
X1,
X2,
X3,
X4,
X5,
X6 being
set holds
( not
X1 in X2 or not
X2 in X3 or not
X3 in X4 or not
X4 in X5 or not
X5 in X6 or not
X6 in X1 )
theorem Th7:
for
Y,
X being
set st
Y in X holds
not
X c= Y
:: deftheorem defines succ ORDINAL1:def 1 :
theorem
canceled;
theorem
canceled;
theorem Th10:
theorem
canceled;
theorem
theorem Th13:
for
x,
X being
set holds
(
x in succ X iff (
x in X or
x = X ) )
theorem Th14:
:: deftheorem Def2 defines epsilon-transitive ORDINAL1:def 2 :
:: deftheorem Def3 defines epsilon-connected ORDINAL1:def 3 :
Lm1:
( {} is epsilon-transitive & {} is epsilon-connected )
:: deftheorem Def4 defines ordinal ORDINAL1:def 4 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th19:
theorem
canceled;
theorem Th21:
theorem
theorem Th23:
theorem Th24:
:: deftheorem defines c= ORDINAL1:def 5 :
theorem
theorem Th26:
theorem
canceled;
theorem
canceled;
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
for
X being
set holds
not for
x being
set holds
(
x in X iff
x is
Ordinal )
theorem Th38:
theorem
:: deftheorem Def6 defines limit_ordinal ORDINAL1:def 6 :
theorem
canceled;
theorem Th41:
theorem
:: deftheorem Def7 defines T-Sequence-like ORDINAL1:def 7 :
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
:: deftheorem ORDINAL1:def 8 :
canceled;
theorem
:: deftheorem Def9 defines c=-linear ORDINAL1:def 9 :
theorem
theorem
begin
:: deftheorem Def10 defines On ORDINAL1:def 10 :
for
X,
b2 being
set holds
(
b2 = On X iff for
x being
set holds
(
x in b2 iff (
x in X &
x is
Ordinal ) ) );
:: deftheorem defines Lim ORDINAL1:def 11 :
theorem Th51:
:: deftheorem Def12 defines omega ORDINAL1:def 12 :
:: deftheorem Def13 defines natural ORDINAL1:def 13 :
theorem