:: ORDINAL1 semantic presentation

begin


theorem :: ORDINAL1:1
canceled;

theorem :: ORDINAL1:2
canceled;

theorem :: ORDINAL1:3
canceled;

theorem :: ORDINAL1:4
canceled;

theorem Th5: :: ORDINAL1:5
for Y, X being set st Y in X holds
not X c= Y
proof
let Y, X be set ; ::_thesis: ( Y in X implies not X c= Y )
assume A1: Y in X ; ::_thesis: not X c= Y
assume  X c= Y ; ::_thesis: contradiction
then  Y in Y by A1;
hence  contradiction ; ::_thesis: verum
end;

definition
let X be set ;
func succ X ->  set  equals :: ORDINAL1:def 1
X \/ {X};
coherence
 X \/ {X} is set ;
end;

:: deftheorem  defines succ ORDINAL1:def_1_:_
 for X being set holds succ X = X \/ {X};

registration
let X be set ;
cluster succ X ->  non empty ;
coherence
 not succ X is empty ;
end;

theorem Th6: :: ORDINAL1:6
for X being set holds X in succ X
proof
let X be set ; ::_thesis: X in succ X
 X in {X} by TARSKI:def_1;
hence  X in succ X by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: ORDINAL1:7
for X, Y being set st succ X = succ Y holds
X = Y
proof
let X, Y be set ; ::_thesis: ( succ X = succ Y implies X = Y )
assume that
A1: succ X = succ Y and
A2: X <> Y ; ::_thesis: contradiction
 Y in X \/ {X} by A1, Th6;
then A3: ( Y in X or Y in {X} ) by XBOOLE_0:def_3;
 X in Y \/ {Y} by A1, Th6;
then  ( X in Y or X in {Y} ) by XBOOLE_0:def_3;
hence  contradiction by A2, A3, TARSKI:def_1; ::_thesis: verum
end;

theorem Th8: :: ORDINAL1:8
for x, X being set holds
( x in succ X iff ( x in X or x = X ) )
proof
let x, X be set ; ::_thesis: ( x in succ X iff ( x in X or x = X ) )
thus  ( not x in succ X or x in X or x = X ) ::_thesis: ( ( x in X or x = X ) implies x in succ X )
proof
assume  x in succ X ; ::_thesis: ( x in X or x = X )
then  ( x in X or x in {X} ) by XBOOLE_0:def_3;
hence  ( x in X or x = X ) by TARSKI:def_1; ::_thesis: verum
end;
assume  ( x in X or x = X ) ; ::_thesis: x in succ X
then  ( x in X or x in {X} ) by TARSKI:def_1;
hence  x in succ X by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th9: :: ORDINAL1:9
for X being set holds X <> succ X
proof
let X be set ; ::_thesis: X <> succ X
assume A1: X = succ X ; ::_thesis: contradiction
 X in succ X by Th6;
hence  contradiction by A1; ::_thesis: verum
end;


definition
let X be set ;
attrX is epsilon-transitive  means :Def2: :: ORDINAL1:def 2
 for x being set st x in X holds
x c= X;
attrX is epsilon-connected  means :Def3: :: ORDINAL1:def 3
 for x, y being set st x in X & y in X & not x in y & not x = y holds
y in x;
end;

:: deftheorem Def2 defines epsilon-transitive ORDINAL1:def_2_:_
 for X being set holds
( X is epsilon-transitive iff for x being set st x in X holds
x c= X );

:: deftheorem Def3 defines epsilon-connected ORDINAL1:def_3_:_
 for X being set holds
( X is epsilon-connected iff for x, y being set st x in X & y in X & not x in y & not x = y holds
y in x );

Lm1:  ( {} is epsilon-transitive & {} is epsilon-connected )
proof
thus  for x being set st x in {} holds
x c= {} ; :: according to ORDINAL1:def_2 ::_thesis: {} is epsilon-connected
thus  for x, y being set st x in {} & y in {} & not x in y & not x = y holds
y in x ; :: according to ORDINAL1:def_3 ::_thesis: verum
end;

definition
let IT be set ;
attrIT is ordinal  means :Def4: :: ORDINAL1:def 4
( IT is epsilon-transitive & IT is epsilon-connected );
end;

:: deftheorem Def4 defines ordinal ORDINAL1:def_4_:_
 for IT being set holds
( IT is ordinal iff ( IT is epsilon-transitive & IT is epsilon-connected ) );

registration
cluster ordinal  ->  epsilon-transitive epsilon-connected for number ;
coherence
 for b1 being set st b1 is ordinal holds
( b1 is epsilon-transitive & b1 is epsilon-connected ) by Def4;
cluster epsilon-transitive epsilon-connected  ->  ordinal for number ;
coherence
 for b1 being set st b1 is epsilon-transitive & b1 is epsilon-connected holds
b1 is ordinal by Def4;
end;

notation
synonym  number for  set ;
end;

registration
cluster ordinal for number ;
existence
 ex b1 being number st b1 is ordinal by Lm1;
end;

definition
mode Ordinal is ordinal number ;
end;


theorem Th10: :: ORDINAL1:10
for A, B being set
for C being epsilon-transitive set st A in B & B in C holds
A in C
proof
let A, B be set ; ::_thesis: for C being epsilon-transitive set st A in B & B in C holds
A in C
let C be epsilon-transitive set ; ::_thesis: ( A in B & B in C implies A in C )
assume that
A1: A in B and
A2: B in C ; ::_thesis: A in C
 B c= C by A2, Def2;
hence  A in C by A1; ::_thesis: verum
end;

theorem Th11: :: ORDINAL1:11
for x being epsilon-transitive set
for A being Ordinal st x c< A holds
x in A
proof
let x be epsilon-transitive set ; ::_thesis: for A being Ordinal st x c< A holds
x in A
let A be Ordinal; ::_thesis: ( x c< A implies x in A )
set a = the Element of A \ x;
assume A1: x c< A ; ::_thesis: x in A
then A2: x c= A by XBOOLE_0:def_8;
 A \ x <> {}
proof
assume  A \ x = {} ; ::_thesis: contradiction
then  A c= x by XBOOLE_1:37;
hence  contradiction by A1, XBOOLE_1:60; ::_thesis: verum
end;
then  the Element of A \ x in A \ x ;
then consider y being set  such that
A3: y in A \ x and
A4: for a being set holds
( not a in A \ x or not a in y ) by TARSKI:2;
A5: not y in x by A3, XBOOLE_0:def_5;
now__::_thesis:_for_a_being_set_st_a_in_x_holds_
a_in_y
let a be set ; ::_thesis: ( a in x implies a in y )
assume  a in x ; ::_thesis: a in y
then consider z being set  such that
A6: z = a and
A7: z in x ;
 z c= x by A7, Def2;
then  not y in z by A3, XBOOLE_0:def_5;
hence  a in y by A2, A3, A5, A6, A7, Def3; ::_thesis: verum
end;
then A8: x c= y by TARSKI:def_3;
A9: y c= A by A3, Def2;
now__::_thesis:_for_a_being_set_st_a_in_y_holds_
a_in_x
let a be set ; ::_thesis: ( a in y implies a in x )
assume A10: a in y ; ::_thesis: a in x
then  not a in A \ x by A4;
hence  a in x by A9, A10, XBOOLE_0:def_5; ::_thesis: verum
end;
then A11: y c= x by TARSKI:def_3;
 y in A by A3;
hence  x in A by A11, A8, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: ORDINAL1:12
for A being epsilon-transitive set
for B, C being Ordinal st A c= B & B in C holds
A in C
proof
let A be epsilon-transitive set ; ::_thesis: for B, C being Ordinal st A c= B & B in C holds
A in C
let B, C be Ordinal; ::_thesis: ( A c= B & B in C implies A in C )
assume that
A1: A c= B and
A2: B in C ; ::_thesis: A in C
 B c= C by A2, Def2;
then A3: A c= C by A1, XBOOLE_1:1;
 A <> C by A1, A2, Th5;
then  A c< C by A3, XBOOLE_0:def_8;
hence  A in C by Th11; ::_thesis: verum
end;

theorem Th13: :: ORDINAL1:13
for a being set
for A being Ordinal st a in A holds
a is Ordinal
proof
let a be set ; ::_thesis: for A being Ordinal st a in A holds
a is Ordinal
let A be Ordinal; ::_thesis: ( a in A implies a is Ordinal )
assume A1: a in A ; ::_thesis: a is Ordinal
then A2: a c= A by Def2;
now__::_thesis:_for_y_being_set_st_y_in_a_holds_
y_c=_a
let y be set ; ::_thesis: ( y in a implies y c= a )
assume A3: y in a ; ::_thesis: y c= a
then A4: y c= A by A2, Def2;
assume  not y c= a ; ::_thesis: contradiction
then consider b being set  such that
A5: ( b in y & not b in a ) by TARSKI:def_3;
 b in y \ a by A5, XBOOLE_0:def_5;
then consider z being set  such that
A6: z in y \ a and
 for c being set holds
( not c in y \ a or not c in z ) by TARSKI:2;
 z in y by A6;
then  ( z in a or z = a or a in z ) by A1, A4, Def3;
hence  contradiction by A3, A6, XREGULAR:7, XBOOLE_0:def_5; ::_thesis: verum
end;
then A7: a is epsilon-transitive by Def2;
 for y, z being set st y in a & z in a & not y in z & not y = z holds
z in y by A2, Def3;
then  a is epsilon-connected by Def3;
hence  a is Ordinal by A7; ::_thesis: verum
end;

theorem Th14: :: ORDINAL1:14
for A, B being Ordinal holds
( A in B or A = B or B in A )
proof
let A, B be Ordinal; ::_thesis: ( A in B or A = B or B in A )
assume that
A1: not A in B and
A2: A <> B ; ::_thesis: B in A
 not A c< B by A1, Th11;
then  not A c= B by A2, XBOOLE_0:def_8;
then consider a being set  such that
A3: ( a in A & not a in B ) by TARSKI:def_3;
 a in A \ B by A3, XBOOLE_0:def_5;
then consider X being set  such that
A4: X in A \ B and
A5: for a being set holds
( not a in A \ B or not a in X ) by TARSKI:2;
A6: X c= A by A4, Def2;
now__::_thesis:_for_b_being_set_st_b_in_X_holds_
b_in_B
let b be set ; ::_thesis: ( b in X implies b in B )
assume A7: b in X ; ::_thesis: b in B
then  not b in A \ B by A5;
hence  b in B by A6, A7, XBOOLE_0:def_5; ::_thesis: verum
end;
then  X c= B by TARSKI:def_3;
then A8: ( X c< B or X = B ) by XBOOLE_0:def_8;
 ( not X in B & X is Ordinal ) by A4, Th13, XBOOLE_0:def_5;
hence  B in A by A4, A8, Th11; ::_thesis: verum
end;

definition
let A, B be Ordinal;
:: original: c=
redefine predA c= B means :: ORDINAL1:def 5
 for C being Ordinal st C in A holds
C in B;
compatibility
 ( A c= B iff for C being Ordinal st C in A holds
C in B )
proof
thus  ( A c= B implies for C being Ordinal st C in A holds
C in B ) ; ::_thesis: ( ( for C being Ordinal st C in A holds
C in B ) implies A c= B )
assume A1: for C being Ordinal st C in A holds
C in B ; ::_thesis: A c= B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B )
assume A2: x in A ; ::_thesis: x in B
then reconsider C = x as Ordinal by Th13;
 C in B by A1, A2;
hence  x in B ; ::_thesis: verum
end;
connectedness
 for A, B being Ordinal st ex C being Ordinal st
( C in A & not C in B ) holds
for C being Ordinal st C in B holds
C in A
proof
let A, B be Ordinal; ::_thesis: ( ex C being Ordinal st
( C in A & not C in B ) implies for C being Ordinal st C in B holds
C in A )
given C being Ordinal such that A3: ( C in A & not C in B ) ; ::_thesis: for C being Ordinal st C in B holds
C in A
let D be Ordinal; ::_thesis: ( D in B implies D in A )
 ( A in B or A = B or B in A ) by Th14;
hence  ( D in B implies D in A ) by A3, Th10; ::_thesis: verum
end;
end;

:: deftheorem  defines c= ORDINAL1:def_5_:_
 for A, B being Ordinal holds
( A c= B iff for C being Ordinal st C in A holds
C in B );

theorem :: ORDINAL1:15
for A, B being Ordinal holds A,B are_c=-comparable
proof
let A, B be Ordinal; ::_thesis: A,B are_c=-comparable
 ( A c= B or B c= A ) ;
hence  A,B are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum
end;

theorem Th16: :: ORDINAL1:16
for A, B being Ordinal holds
( A c= B or B in A )
proof
let A, B be Ordinal; ::_thesis: ( A c= B or B in A )
 ( A in B or A = B or B in A ) by Th14;
hence  ( A c= B or B in A ) by Def2; ::_thesis: verum
end;

registration
cluster empty  ->  ordinal for number ;
coherence
 for b1 being number st b1 is empty holds
b1 is ordinal by Lm1;
end;

theorem Th17: :: ORDINAL1:17
for x being set st x is Ordinal holds
succ x is Ordinal
proof
let x be set ; ::_thesis: ( x is Ordinal implies succ x is Ordinal )
A1: now__::_thesis:_for_y_being_set_holds_
(_not_y_in_succ_x_or_y_in_x_or_y_=_x_)
let y be set ; ::_thesis: ( not y in succ x or y in x or y = x )
A2: ( y in {x} implies y = x ) by TARSKI:def_1;
assume  y in succ x ; ::_thesis: ( y in x or y = x )
hence  ( y in x or y = x ) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
assume A3: x is Ordinal ; ::_thesis: succ x is Ordinal
now__::_thesis:_for_y_being_set_st_y_in_succ_x_holds_
y_c=_succ_x
let y be set ; ::_thesis: ( y in succ x implies y c= succ x )
A4: ( y = x implies y c= succ x ) by XBOOLE_1:7;
A5: now__::_thesis:_(_y_in_x_implies_y_c=_succ_x_)
assume  y in x ; ::_thesis: y c= succ x
then A6: y c= x by A3, Def2;
 x c= x \/ {x} by XBOOLE_1:7;
hence  y c= succ x by A6, XBOOLE_1:1; ::_thesis: verum
end;
assume  y in succ x ; ::_thesis: y c= succ x
hence  y c= succ x by A1, A5, A4; ::_thesis: verum
end;
then A7: succ x is epsilon-transitive by Def2;
now__::_thesis:_for_y,_z_being_set_st_y_in_succ_x_&_z_in_succ_x_&_not_y_in_z_&_not_y_=_z_holds_
z_in_y
let y, z be set ; ::_thesis: ( y in succ x & z in succ x & not y in z & not y = z implies z in y )
assume that
A8: y in succ x and
A9: z in succ x ; ::_thesis: ( y in z or y = z or z in y )
A10: ( z in x or z = x ) by A1, A9;
 ( y in x or y = x ) by A1, A8;
hence  ( y in z or y = z or z in y ) by A3, A10, Def3; ::_thesis: verum
end;
then  succ x is epsilon-connected by Def3;
hence  succ x is Ordinal by A7; ::_thesis: verum
end;

theorem Th18: :: ORDINAL1:18
for x being set st x is ordinal holds
union x is ordinal
proof
let x be set ; ::_thesis: ( x is ordinal implies union x is ordinal )
assume  ( x is epsilon-transitive & x is epsilon-connected ) ; :: according to ORDINAL1:def_4 ::_thesis: union x is ordinal
then reconsider A = x as Ordinal ;
thus  for y being set st y in union x holds
y c= union x :: according to ORDINAL1:def_2,ORDINAL1:def_4 ::_thesis: union x is epsilon-connected
proof
let y be set ; ::_thesis: ( y in union x implies y c= union x )
assume  y in union x ; ::_thesis: y c= union x
then consider z being set  such that
A1: y in z and
A2: z in x by TARSKI:def_4;
 z in A by A2;
then reconsider z = z as Ordinal by Th13;
 z c= A by A2, Def2;
hence  y c= union x by A1, ZFMISC_1:74; ::_thesis: verum
end;
let y be set ; :: according to ORDINAL1:def_3 ::_thesis: for y being set st y in union x & y in union x & not y in y & not y = y holds
y in y
let z be set ; ::_thesis: ( y in union x & z in union x & not y in z & not y = z implies z in y )
assume that
A3: y in union x and
A4: z in union x ; ::_thesis: ( y in z or y = z or z in y )
consider X being set  such that
A5: y in X and
A6: X in x by A3, TARSKI:def_4;
A7: X in A by A6;
consider Y being set  such that
A8: z in Y and
A9: Y in x by A4, TARSKI:def_4;
reconsider X = X, Y = Y as Ordinal by A9, A7, Th13;
 z in Y by A8;
then A10: z is Ordinal by Th13;
 y in X by A5;
then  y is Ordinal by Th13;
hence  ( y in z or y = z or z in y ) by A10, Th14; ::_thesis: verum
end;

registration
cluster non empty epsilon-transitive epsilon-connected ordinal for number ;
existence
 not for b1 being Ordinal holds b1 is empty
proof
reconsider A = succ {} as Ordinal by Th17;
take  A ; ::_thesis: not A is empty
thus  not A is empty ; ::_thesis: verum
end;
end;

registration
let A be Ordinal;
cluster succ A ->  non empty ordinal ;
coherence
 ( not succ A is empty & succ A is ordinal ) by Th17;
cluster union A ->  ordinal ;
coherence
 union A is ordinal by Th18;
end;

theorem Th19: :: ORDINAL1:19
for X being set st ( for x being set st x in X holds
( x is Ordinal & x c= X ) ) holds
X is ordinal
proof
let X be set ; ::_thesis: ( ( for x being set st x in X holds
( x is Ordinal & x c= X ) ) implies X is ordinal )
assume A1: for x being set st x in X holds
( x is Ordinal & x c= X ) ; ::_thesis: X is ordinal
thus  X is epsilon-transitive :: according to ORDINAL1:def_4 ::_thesis: X is epsilon-connected
proof
let x be set ; :: according to ORDINAL1:def_2 ::_thesis: ( x in X implies x c= X )
assume  x in X ; ::_thesis: x c= X
hence  x c= X by A1; ::_thesis: verum
end;
let x be set ; :: according to ORDINAL1:def_3 ::_thesis: for y being set st x in X & y in X & not x in y & not x = y holds
y in x
let y be set ; ::_thesis: ( x in X & y in X & not x in y & not x = y implies y in x )
assume  ( x in X & y in X ) ; ::_thesis: ( x in y or x = y or y in x )
then  ( x is Ordinal & y is Ordinal ) by A1;
hence  ( x in y or x = y or y in x ) by Th14; ::_thesis: verum
end;

theorem Th20: :: ORDINAL1:20
for X being set
for A being Ordinal st X c= A & X <> {} holds
ex C being Ordinal st
( C in X & ( for B being Ordinal st B in X holds
C c= B ) )
proof
let X be set ; ::_thesis: for A being Ordinal st X c= A & X <> {} holds
ex C being Ordinal st
( C in X & ( for B being Ordinal st B in X holds
C c= B ) )
let A be Ordinal; ::_thesis: ( X c= A & X <> {} implies ex C being Ordinal st
( C in X & ( for B being Ordinal st B in X holds
C c= B ) ) )
set a = the Element of X;
assume that
A1: X c= A and
A2: X <> {} ; ::_thesis: ex C being Ordinal st
( C in X & ( for B being Ordinal st B in X holds
C c= B ) )
 the Element of X in X by A2;
then consider Y being set  such that
A3: Y in X and
A4: for a being set holds
( not a in X or not a in Y ) by TARSKI:2;
 Y is Ordinal by A1, A3, Th13;
then consider C being Ordinal such that
A5: C = Y ;
take  C ; ::_thesis: ( C in X & ( for B being Ordinal st B in X holds
C c= B ) )
thus  C in X by A3, A5; ::_thesis: for B being Ordinal st B in X holds
C c= B
let B be Ordinal; ::_thesis: ( B in X implies C c= B )
assume  B in X ; ::_thesis: C c= B
then  not B in C by A4, A5;
then  ( B = C or C in B ) by Th14;
hence  C c= B by Def2; ::_thesis: verum
end;

theorem Th21: :: ORDINAL1:21
for A, B being Ordinal holds
( A in B iff succ A c= B )
proof
let A, B be Ordinal; ::_thesis: ( A in B iff succ A c= B )
thus  ( A in B implies succ A c= B ) ::_thesis: ( succ A c= B implies A in B )
proof
assume A1: A in B ; ::_thesis: succ A c= B
then  for a being set st a in {A} holds
a in B by TARSKI:def_1;
then A2: {A} c= B by TARSKI:def_3;
 A c= B by A1, Def2;
hence  succ A c= B by A2, XBOOLE_1:8; ::_thesis: verum
end;
assume A3: succ A c= B ; ::_thesis: A in B
 A in succ A by Th6;
hence  A in B by A3; ::_thesis: verum
end;

theorem Th22: :: ORDINAL1:22
for A, C being Ordinal holds
( A in succ C iff A c= C )
proof
let A, C be Ordinal; ::_thesis: ( A in succ C iff A c= C )
thus  ( A in succ C implies A c= C ) ::_thesis: ( A c= C implies A in succ C )
proof
assume  A in succ C ; ::_thesis: A c= C
then  ( A in C or A in {C} ) by XBOOLE_0:def_3;
hence  A c= C by Def2, TARSKI:def_1; ::_thesis: verum
end;
assume A1: A c= C ; ::_thesis: A in succ C
assume  not A in succ C ; ::_thesis: contradiction
then  ( A = succ C or succ C in A ) by Th14;
then A2: succ C c= C by A1, Def2;
 C in succ C by Th6;
then  C c= succ C by Def2;
then  succ C = C by A2, XBOOLE_0:def_10;
hence  contradiction by Th9; ::_thesis: verum
end;

scheme :: ORDINAL1:sch 1
OrdinalMin{ P1[ Ordinal] } :
 ex A being Ordinal st
( P1[A] & ( for B being Ordinal st P1[B] holds
A c= B ) )
provided
A1: ex A being Ordinal st P1[A]
proof
consider A being Ordinal such that
A2: P1[A] by A1;
defpred S1[ set ] means  ex B being Ordinal st
( $1 = B & P1[B] );
consider X being set  such that
A3: for x being set holds
( x in X iff ( x in succ A & S1[x] ) ) from XBOOLE_0:sch_1();
 for a being set st a in X holds
a in succ A by A3;
then A4: X c= succ A by TARSKI:def_3;
 A in succ A by Th6;
then  X <> {} by A2, A3;
then consider C being Ordinal such that
A5: C in X and
A6: for B being Ordinal st B in X holds
C c= B by A4, Th20;
 C in succ A by A3, A5;
then A7: C c= succ A by Def2;
take  C ; ::_thesis: ( P1[C] & ( for B being Ordinal st P1[B] holds
C c= B ) )
 ex B being Ordinal st
( C = B & P1[B] ) by A3, A5;
hence  P1[C] ; ::_thesis: for B being Ordinal st P1[B] holds
C c= B
let B be Ordinal; ::_thesis: ( P1[B] implies C c= B )
assume A8: P1[B] ; ::_thesis: C c= B
assume A9: not C c= B ; ::_thesis: contradiction
then  B c< C by XBOOLE_0:def_8;
then  B in C by Th11;
then  B in X by A3, A8, A7;
hence  contradiction by A6, A9; ::_thesis: verum
end;

scheme :: ORDINAL1:sch 2
TransfiniteInd{ P1[ Ordinal] } :
 for A being Ordinal holds P1[A]
provided
A1: for A being Ordinal st ( for C being Ordinal st C in A holds
P1[C] ) holds
P1[A]
proof
defpred S1[ set ] means  ex B being Ordinal st
( $1 = B & P1[B] );
let A be Ordinal; ::_thesis: P1[A]
set Y = succ A;
consider Z being set  such that
A2: for x being set holds
( x in Z iff ( x in succ A & S1[x] ) ) from XBOOLE_0:sch_1();
now__::_thesis:_not_(succ_A)_\_Z_<>_{}
assume  (succ A) \ Z <> {} ; ::_thesis: contradiction
then consider C being Ordinal such that
A3: C in (succ A) \ Z and
A4: for B being Ordinal st B in (succ A) \ Z holds
C c= B by Th20;
now__::_thesis:_for_B_being_Ordinal_st_B_in_C_holds_
P1[B]
let B be Ordinal; ::_thesis: ( B in C implies P1[B] )
assume A5: B in C ; ::_thesis: P1[B]
A6: C c= succ A by A3, Def2;
now__::_thesis:_B_in_Z
assume  not B in Z ; ::_thesis: contradiction
then  B in (succ A) \ Z by A5, A6, XBOOLE_0:def_5;
then A7: C c= B by A4;
 C <> B by A5;
then  C c< B by A7, XBOOLE_0:def_8;
hence  contradiction by A5, Th11; ::_thesis: verum
end;
then  ex B9 being Ordinal st
( B = B9 & P1[B9] ) by A2;
hence  P1[B] ; ::_thesis: verum
end;
then A8: P1[C] by A1;
 not C in Z by A3, XBOOLE_0:def_5;
hence  contradiction by A2, A3, A8; ::_thesis: verum
end;
then  ( not A in succ A or A in Z ) by XBOOLE_0:def_5;
then  ex B being Ordinal st
( A = B & P1[B] ) by A2, Th6;
hence  P1[A] ; ::_thesis: verum
end;

theorem Th23: :: ORDINAL1:23
for X being set st ( for a being set st a in X holds
a is Ordinal ) holds
union X is ordinal
proof
let X be set ; ::_thesis: ( ( for a being set st a in X holds
a is Ordinal ) implies union X is ordinal )
assume A1: for a being set st a in X holds
a is Ordinal ; ::_thesis: union X is ordinal
thus  union X is epsilon-transitive :: according to ORDINAL1:def_4 ::_thesis: union X is epsilon-connected
proof
let x be set ; :: according to ORDINAL1:def_2 ::_thesis: ( x in union X implies x c= union X )
assume  x in union X ; ::_thesis: x c= union X
then consider Y being set  such that
A2: x in Y and
A3: Y in X by TARSKI:def_4;
 Y is Ordinal by A1, A3;
then A4: x c= Y by A2, Def2;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in x or a in union X )
assume  a in x ; ::_thesis: a in union X
hence  a in union X by A3, A4, TARSKI:def_4; ::_thesis: verum
end;
let x be set ; :: according to ORDINAL1:def_3 ::_thesis: for y being set st x in union X & y in union X & not x in y & not x = y holds
y in x
let y be set ; ::_thesis: ( x in union X & y in union X & not x in y & not x = y implies y in x )
assume that
A5: x in union X and
A6: y in union X ; ::_thesis: ( x in y or x = y or y in x )
consider Z being set  such that
A7: y in Z and
A8: Z in X by A6, TARSKI:def_4;
 Z is Ordinal by A1, A8;
then A9: y is Ordinal by A7, Th13;
consider Y being set  such that
A10: x in Y and
A11: Y in X by A5, TARSKI:def_4;
 Y is Ordinal by A1, A11;
then  x is Ordinal by A10, Th13;
hence  ( x in y or x = y or y in x ) by A9, Th14; ::_thesis: verum
end;

theorem Th24: :: ORDINAL1:24
for X being set st ( for a being set st a in X holds
a is Ordinal ) holds
ex A being Ordinal st X c= A
proof
let X be set ; ::_thesis: ( ( for a being set st a in X holds
a is Ordinal ) implies ex A being Ordinal st X c= A )
assume A1: for a being set st a in X holds
a is Ordinal ; ::_thesis: ex A being Ordinal st X c= A
then A2: union X is Ordinal by Th23;
then reconsider A = succ (union X) as Ordinal ;
take  A ; ::_thesis: X c= A
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in A )
assume A3: a in X ; ::_thesis: a in A
then reconsider B = a as Ordinal by A1;
 for b being set st b in B holds
b in union X by A3, TARSKI:def_4;
then  B c= union X by TARSKI:def_3;
hence  a in A by A2, Th22; ::_thesis: verum
end;

theorem Th25: :: ORDINAL1:25
for X being set holds
not for x being set holds
( x in X iff x is Ordinal )
proof
given X being set  such that A1: for x being set holds
( x in X iff x is Ordinal ) ; ::_thesis: contradiction
A2: X is epsilon-transitive
proof
let x be set ; :: according to ORDINAL1:def_2 ::_thesis: ( x in X implies x c= X )
assume  x in X ; ::_thesis: x c= X
then A3: x is Ordinal by A1;
thus  x c= X ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in x or a in X )
assume  a in x ; ::_thesis: a in X
then  a is Ordinal by A3, Th13;
hence  a in X by A1; ::_thesis: verum
end;
end;
 X is epsilon-connected
proof
let x be set ; :: according to ORDINAL1:def_3 ::_thesis: for y being set st x in X & y in X & not x in y & not x = y holds
y in x
let y be set ; ::_thesis: ( x in X & y in X & not x in y & not x = y implies y in x )
assume  ( x in X & y in X ) ; ::_thesis: ( x in y or x = y or y in x )
then  ( x is Ordinal & y is Ordinal ) by A1;
hence  ( x in y or x = y or y in x ) by Th14; ::_thesis: verum
end;
then  X in X by A1, A2;
hence  contradiction ; ::_thesis: verum
end;

theorem Th26: :: ORDINAL1:26
for X being set holds
not for A being Ordinal holds A in X
proof
defpred S1[ set ] means $1 is Ordinal;
given X being set  such that A1: for A being Ordinal holds A in X ; ::_thesis: contradiction
consider Y being set  such that
A2: for a being set holds
( a in Y iff ( a in X & S1[a] ) ) from XBOOLE_0:sch_1();
now__::_thesis:_for_x_being_set_st_x_is_Ordinal_holds_
x_in_Y
let x be set ; ::_thesis: ( x is Ordinal implies x in Y )
assume A3: x is Ordinal ; ::_thesis: x in Y
then  x in X by A1;
hence  x in Y by A2, A3; ::_thesis: verum
end;
then  for x being set holds
( x in Y iff x is Ordinal ) by A2;
hence  contradiction by Th25; ::_thesis: verum
end;

theorem :: ORDINAL1:27
for X being set ex A being Ordinal st
( not A in X & ( for B being Ordinal st not B in X holds
A c= B ) )
proof
let X be set ; ::_thesis: ex A being Ordinal st
( not A in X & ( for B being Ordinal st not B in X holds
A c= B ) )
defpred S1[ set ] means  not $1 in X;
consider B being Ordinal such that
A1: not B in X by Th26;
consider Y being set  such that
A2: for a being set holds
( a in Y iff ( a in succ B & S1[a] ) ) from XBOOLE_0:sch_1();
 for a being set st a in Y holds
a in succ B by A2;
then A3: Y c= succ B by TARSKI:def_3;
 B in succ B by Th6;
then  Y <> {} by A1, A2;
then consider A being Ordinal such that
A4: A in Y and
A5: for B being Ordinal st B in Y holds
A c= B by A3, Th20;
 A in succ B by A2, A4;
then A6: A c= succ B by Def2;
take  A ; ::_thesis: ( not A in X & ( for B being Ordinal st not B in X holds
A c= B ) )
thus  not A in X by A2, A4; ::_thesis: for B being Ordinal st not B in X holds
A c= B
let C be Ordinal; ::_thesis: ( not C in X implies A c= C )
assume A7: not C in X ; ::_thesis: A c= C
assume A8: not A c= C ; ::_thesis: contradiction
then  not A in C by Def2;
then  C in A by A8, Th14;
then  C in Y by A2, A7, A6;
hence  contradiction by A5, A8; ::_thesis: verum
end;

definition
let A be set ;
attrA is limit_ordinal  means :Def6: :: ORDINAL1:def 6
A = union A;
end;

:: deftheorem Def6 defines limit_ordinal ORDINAL1:def_6_:_
 for A being set holds
( A is limit_ordinal iff A = union A );

theorem Th28: :: ORDINAL1:28
for A being Ordinal holds
( A is limit_ordinal iff for C being Ordinal st C in A holds
succ C in A )
proof
let A be Ordinal; ::_thesis: ( A is limit_ordinal iff for C being Ordinal st C in A holds
succ C in A )
thus  ( A is limit_ordinal implies for C being Ordinal st C in A holds
succ C in A ) ::_thesis: ( ( for C being Ordinal st C in A holds
succ C in A ) implies A is limit_ordinal )
proof
assume  A is limit_ordinal ; ::_thesis: for C being Ordinal st C in A holds
succ C in A
then A1: A = union A by Def6;
let C be Ordinal; ::_thesis: ( C in A implies succ C in A )
assume  C in A ; ::_thesis: succ C in A
then consider z being set  such that
A2: C in z and
A3: z in A by A1, TARSKI:def_4;
 for b being set st b in {C} holds
b in z by A2, TARSKI:def_1;
then A4: {C} c= z by TARSKI:def_3;
A5: z is Ordinal by A3, Th13;
then  C c= z by A2, Def2;
then  succ C c= z by A4, XBOOLE_1:8;
then  ( succ C = z or succ C c< z ) by XBOOLE_0:def_8;
then A6: ( succ C = z or succ C in z ) by A5, Th11;
 z c= A by A3, Def2;
hence  succ C in A by A3, A6; ::_thesis: verum
end;
assume A7: for C being Ordinal st C in A holds
succ C in A ; ::_thesis: A is limit_ordinal
now__::_thesis:_for_a_being_set_st_a_in_A_holds_
a_in_union_A
let a be set ; ::_thesis: ( a in A implies a in union A )
assume A8: a in A ; ::_thesis: a in union A
then  a is Ordinal by Th13;
then A9: succ a in A by A7, A8;
 a in succ a by Th6;
hence  a in union A by A9, TARSKI:def_4; ::_thesis: verum
end;
then A10: A c= union A by TARSKI:def_3;
now__::_thesis:_for_a_being_set_st_a_in_union_A_holds_
a_in_A
let a be set ; ::_thesis: ( a in union A implies a in A )
assume  a in union A ; ::_thesis: a in A
then consider z being set  such that
A11: a in z and
A12: z in A by TARSKI:def_4;
 z c= A by A12, Def2;
hence  a in A by A11; ::_thesis: verum
end;
then  union A c= A by TARSKI:def_3;
then  A = union A by A10, XBOOLE_0:def_10;
hence  A is limit_ordinal by Def6; ::_thesis: verum
end;

theorem :: ORDINAL1:29
for A being Ordinal holds
( not A is limit_ordinal iff ex B being Ordinal st A = succ B )
proof
let A be Ordinal; ::_thesis: ( not A is limit_ordinal iff ex B being Ordinal st A = succ B )
thus  ( not A is limit_ordinal implies ex B being Ordinal st A = succ B ) ::_thesis: ( ex B being Ordinal st A = succ B implies not A is limit_ordinal )
proof
assume  not A is limit_ordinal ; ::_thesis: ex B being Ordinal st A = succ B
then consider B being Ordinal such that
A1: B in A and
A2: not succ B in A by Th28;
take  B ; ::_thesis: A = succ B
assume A3: A <> succ B ; ::_thesis: contradiction
 succ B c= A by A1, Th21;
then  succ B c< A by A3, XBOOLE_0:def_8;
hence  contradiction by A2, Th11; ::_thesis: verum
end;
given B being Ordinal such that A4: A = succ B ; ::_thesis: not A is limit_ordinal
 ( B in A & not succ B in A ) by A4, Th6;
hence  not A is limit_ordinal by Th28; ::_thesis: verum
end;


definition
let IT be set ;
attrIT is T-Sequence-like  means :Def7: :: ORDINAL1:def 7
 proj1 IT is ordinal ;
end;

:: deftheorem Def7 defines T-Sequence-like ORDINAL1:def_7_:_
 for IT being set holds
( IT is T-Sequence-like iff proj1 IT is ordinal );

registration
cluster empty  ->  T-Sequence-like for number ;
coherence
 for b1 being set st b1 is empty holds
b1 is T-Sequence-like
proof
let E be set ; ::_thesis: ( E is empty implies E is T-Sequence-like )
assume  E is empty ; ::_thesis: E is T-Sequence-like
then  proj1 E = {} ;
hence  E is T-Sequence-like by Def7; ::_thesis: verum
end;
end;

definition
mode T-Sequence is T-Sequence-like Function;
end;

registration
let Z be set ;
cluster Relation-like Z -valued Function-like T-Sequence-like for number ;
existence
 ex b1 being T-Sequence st b1 is Z -valued
proof
reconsider L = {} as T-Sequence ;
take  L ; ::_thesis: L is Z -valued
 rng {} = {} ;
hence  rng L c= Z by XBOOLE_1:2; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;

definition
let Z be set ;
mode T-Sequence of Z is Z -valued T-Sequence;
end;

theorem :: ORDINAL1:30
for Z being set holds {} is T-Sequence of Z
proof
let Z be set ; ::_thesis: {} is T-Sequence of Z
reconsider L = {} as T-Sequence ;
 rng L = {} ;
then  rng L c= Z by XBOOLE_1:2;
hence  {} is T-Sequence of Z by RELAT_1:def_19; ::_thesis: verum
end;


theorem :: ORDINAL1:31
for F being Function st dom F is Ordinal holds
F is T-Sequence of rng F by Def7, RELAT_1:def_19;

registration
let L be T-Sequence;
cluster proj1 L ->  ordinal ;
coherence
 dom L is ordinal by Def7;
end;

theorem :: ORDINAL1:32
for X, Y being set st X c= Y holds
for L being T-Sequence of X holds L is T-Sequence of Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies for L being T-Sequence of X holds L is T-Sequence of Y )
assume A1: X c= Y ; ::_thesis: for L being T-Sequence of X holds L is T-Sequence of Y
let L be T-Sequence of X; ::_thesis: L is T-Sequence of Y
 rng L c= X by RELAT_1:def_19;
then  rng L c= Y by A1, XBOOLE_1:1;
hence  L is T-Sequence of Y by RELAT_1:def_19; ::_thesis: verum
end;

registration
let L be T-Sequence;
let A be Ordinal;
clusterL | A ->  rng L -valued T-Sequence-like ;
coherence
 ( L | A is rng L -valued & L | A is T-Sequence-like )
proof
A1: rng (L | A) c= rng L by RELAT_1:70;
 ( A c= dom L implies dom (L | A) = A ) by RELAT_1:62;
hence  ( L | A is rng L -valued & L | A is T-Sequence-like ) by A1, Def7, RELAT_1:68, RELAT_1:def_19; ::_thesis: verum
end;
end;

theorem :: ORDINAL1:33
for X being set
for L being T-Sequence of X
for A being Ordinal holds L | A is T-Sequence of X ;

definition
let IT be set ;
attrIT is c=-linear  means :Def8: :: ORDINAL1:def 8
 for x, y being set st x in IT & y in IT holds
x,y are_c=-comparable ;
end;

:: deftheorem Def8 defines c=-linear ORDINAL1:def_8_:_
 for IT being set holds
( IT is c=-linear iff for x, y being set st x in IT & y in IT holds
x,y are_c=-comparable );

theorem :: ORDINAL1:34
for X being set st ( for a being set st a in X holds
a is T-Sequence ) & X is c=-linear holds
union X is T-Sequence
proof
let X be set ; ::_thesis: ( ( for a being set st a in X holds
a is T-Sequence ) & X is c=-linear implies union X is T-Sequence )
assume that
A1: for a being set st a in X holds
a is T-Sequence and
A2: X is c=-linear ; ::_thesis: union X is T-Sequence
 ( union X is Relation-like & union X is Function-like )
proof
thus  for a being set st a in union X holds
ex b, c being set st [b,c] = a :: according to RELAT_1:def_1 ::_thesis: union X is Function-like
proof
let a be set ; ::_thesis: ( a in union X implies ex b, c being set st [b,c] = a )
assume  a in union X ; ::_thesis: ex b, c being set st [b,c] = a
then consider x being set  such that
A3: a in x and
A4: x in X by TARSKI:def_4;
reconsider x = x as T-Sequence by A1, A4;
 for a being set st a in x holds
ex b, c being set st [b,c] = a by RELAT_1:def_1;
hence  ex b, c being set st [b,c] = a by A3; ::_thesis: verum
end;
let a be set ; :: according to FUNCT_1:def_1 ::_thesis: for b1, b2 being number holds
( not [a,b1] in union X or not [a,b2] in union X or b1 = b2 )
let b, c be set ; ::_thesis: ( not [a,b] in union X or not [a,c] in union X or b = c )
assume that
A5: [a,b] in union X and
A6: [a,c] in union X ; ::_thesis: b = c
consider y being set  such that
A7: [a,c] in y and
A8: y in X by A6, TARSKI:def_4;
reconsider y = y as T-Sequence by A1, A8;
consider x being set  such that
A9: [a,b] in x and
A10: x in X by A5, TARSKI:def_4;
reconsider x = x as T-Sequence by A1, A10;
 x,y are_c=-comparable by A2, A10, A8, Def8;
then  ( x c= y or y c= x ) by XBOOLE_0:def_9;
hence  b = c by A9, A7, FUNCT_1:def_1; ::_thesis: verum
end;
then reconsider F = union X as Function ;
defpred S1[ set , set ] means ( $1 in X & ( for L being T-Sequence st L = $1 holds
dom L = $2 ) );
A11: for a, b, c being set st S1[a,b] & S1[a,c] holds
b = c
proof
let a, b, c be set ; ::_thesis: ( S1[a,b] & S1[a,c] implies b = c )
assume that
A12: a in X and
A13: for L being T-Sequence st L = a holds
dom L = b and
 a in X and
A14: for L being T-Sequence st L = a holds
dom L = c ; ::_thesis: b = c
reconsider a = a as T-Sequence by A1, A12;
 dom a = b by A13;
hence  b = c by A14; ::_thesis: verum
end;
consider G being Function such that
A15: for a, b being set holds
( [a,b] in G iff ( a in X & S1[a,b] ) ) from FUNCT_1:sch_1(A11);
A16: for a, b being set st [a,b] in G holds
b is Ordinal
proof
let a, b be set ; ::_thesis: ( [a,b] in G implies b is Ordinal )
assume A17: [a,b] in G ; ::_thesis: b is Ordinal
then  a in X by A15;
then reconsider a = a as T-Sequence by A1;
 dom a = b by A15, A17;
hence  b is Ordinal ; ::_thesis: verum
end;
 for a being set st a in rng G holds
a is Ordinal
proof
let a be set ; ::_thesis: ( a in rng G implies a is Ordinal )
assume  a in rng G ; ::_thesis: a is Ordinal
then consider b being set  such that
A18: ( b in dom G & a = G . b ) by FUNCT_1:def_3;
 [b,a] in G by A18, FUNCT_1:1;
hence  a is Ordinal by A16; ::_thesis: verum
end;
then consider A being Ordinal such that
A19: rng G c= A by Th24;
defpred S2[ Ordinal] means  for B being Ordinal st B in rng G holds
B c= $1;
 for B being Ordinal st B in rng G holds
B c= A by A19, Def2;
then A20: ex A being Ordinal st S2[A] ;
consider A being Ordinal such that
A21: ( S2[A] & ( for C being Ordinal st S2[C] holds
A c= C ) ) from ORDINAL1:sch_1(A20);
 dom F = A
proof
thus  for a being set st a in dom F holds
a in A :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: A c= dom F
proof
let a be set ; ::_thesis: ( a in dom F implies a in A )
assume  a in dom F ; ::_thesis: a in A
then consider b being set  such that
A22: [a,b] in F by XTUPLE_0:def_12;
consider x being set  such that
A23: [a,b] in x and
A24: x in X by A22, TARSKI:def_4;
reconsider x = x as T-Sequence by A1, A24;
 for L being T-Sequence st L = x holds
dom L = dom x ;
then  [x,(dom x)] in G by A15, A24;
then  ( x in dom G & dom x = G . x ) by FUNCT_1:1;
then  dom x in rng G by FUNCT_1:def_3;
then A25: dom x c= A by A21;
 a in dom x by A23, XTUPLE_0:def_12;
hence  a in A by A25; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in dom F )
assume A26: a in A ; ::_thesis: a in dom F
then reconsider a9 = a as Ordinal by Th13;
now__::_thesis:_ex_L_being_T-Sequence_st_
(_L_in_X_&_a9_in_dom_L_)
assume A27: for L being T-Sequence st L in X holds
not a9 in dom L ; ::_thesis: contradiction
now__::_thesis:_for_B_being_Ordinal_st_B_in_rng_G_holds_
B_c=_a9
let B be Ordinal; ::_thesis: ( B in rng G implies B c= a9 )
assume  B in rng G ; ::_thesis: B c= a9
then consider c being set  such that
A28: ( c in dom G & B = G . c ) by FUNCT_1:def_3;
A29: [c,B] in G by A28, FUNCT_1:1;
then  c in X by A15;
then reconsider c = c as T-Sequence by A1;
 ( c in X & dom c = B ) by A15, A29;
hence  B c= a9 by A27, Th16; ::_thesis: verum
end;
then A30: A c= a9 by A21;
 a9 c= A by A26, Def2;
then  A = a by A30, XBOOLE_0:def_10;
hence  contradiction by A26; ::_thesis: verum
end;
then consider L being T-Sequence such that
A31: ( L in X & a in dom L ) ;
 ( L c= F & ex b being set st [a,b] in L ) by A31, XTUPLE_0:def_12, ZFMISC_1:74;
hence  a in dom F by XTUPLE_0:def_12; ::_thesis: verum
end;
hence  union X is T-Sequence by Def7; ::_thesis: verum
end;

scheme :: ORDINAL1:sch 3
TSUniq{ F1() ->  Ordinal, F2( T-Sequence) ->  set , F3() ->  T-Sequence, F4() ->  T-Sequence } :
 F3() = F4()
provided
A1: ( dom F3() = F1() & ( for B being Ordinal
for L being T-Sequence st B in F1() & L = F3() | B holds
F3() . B = F2(L) ) ) and
A2: ( dom F4() = F1() & ( for B being Ordinal
for L being T-Sequence st B in F1() & L = F4() | B holds
F4() . B = F2(L) ) )
proof
defpred S1[ set ] means F3() . $1 <> F4() . $1;
consider X being set  such that
A3: for x being set holds
( x in X iff ( x in F1() & S1[x] ) ) from XBOOLE_0:sch_1();
 for b being set st b in X holds
b in F1() by A3;
then A4: X c= F1() by TARSKI:def_3;
assume  F3() <> F4() ; ::_thesis: contradiction
then  ex a being set st
( a in F1() & F3() . a <> F4() . a ) by A1, A2, FUNCT_1:2;
then  X <> {} by A3;
then consider B being Ordinal such that
A5: B in X and
A6: for C being Ordinal st C in X holds
B c= C by A4, Th20;
A7: B in F1() by A3, A5;
then A8: B c= F1() by Def2;
then A9: dom (F3() | B) = B by A1, RELAT_1:62;
A10: dom (F4() | B) = B by A2, A8, RELAT_1:62;
A11: now__::_thesis:_for_C_being_Ordinal_st_C_in_B_holds_
F3()_._C_=_F4()_._C
let C be Ordinal; ::_thesis: ( C in B implies F3() . C = F4() . C )
assume A12: C in B ; ::_thesis: F3() . C = F4() . C
then  not C in X by A6, Th5;
hence  F3() . C = F4() . C by A3, A8, A12; ::_thesis: verum
end;
now__::_thesis:_for_a_being_set_st_a_in_B_holds_
(F3()_|_B)_._a_=_(F4()_|_B)_._a
let a be set ; ::_thesis: ( a in B implies (F3() | B) . a = (F4() | B) . a )
assume A13: a in B ; ::_thesis: (F3() | B) . a = (F4() | B) . a
then reconsider a9 = a as Ordinal by Th13;
 ( F3() . a9 = F4() . a9 & (F3() | B) . a = F3() . a ) by A11, A9, A13, FUNCT_1:47;
hence  (F3() | B) . a = (F4() | B) . a by A10, A13, FUNCT_1:47; ::_thesis: verum
end;
then A14: F3() | B = F4() | B by A9, A10, FUNCT_1:2;
 ( F3() . B = F2((F3() | B)) & F4() . B = F2((F4() | B)) ) by A1, A2, A7;
hence  contradiction by A3, A5, A14; ::_thesis: verum
end;

scheme :: ORDINAL1:sch 4
TSExist{ F1() ->  Ordinal, F2( T-Sequence) ->  set } :
 ex L being T-Sequence st
( dom L = F1() & ( for B being Ordinal
for L1 being T-Sequence st B in F1() & L1 = L | B holds
L . B = F2(L1) ) )
proof
defpred S1[ Ordinal] means  ex L being T-Sequence st
( dom L = $1 & ( for B being Ordinal st B in $1 holds
L . B = F2((L | B)) ) );
A1: for B being Ordinal st ( for C being Ordinal st C in B holds
S1[C] ) holds
S1[B]
proof
defpred S2[ set , set ] means ( $1 is Ordinal & $2 is T-Sequence & ( for A being Ordinal
for L being T-Sequence st A = $1 & L = $2 holds
( dom L = A & ( for B being Ordinal st B in A holds
L . B = F2((L | B)) ) ) ) );
let B be Ordinal; ::_thesis: ( ( for C being Ordinal st C in B holds
S1[C] ) implies S1[B] )
assume A2: for C being Ordinal st C in B holds
ex L being T-Sequence st
( dom L = C & ( for D being Ordinal st D in C holds
L . D = F2((L | D)) ) ) ; ::_thesis: S1[B]
A3: for a, b, c being set st S2[a,b] & S2[a,c] holds
b = c
proof
let a, b, c be set ; ::_thesis: ( S2[a,b] & S2[a,c] implies b = c )
assume that
A4: a is Ordinal and
A5: b is T-Sequence and
A6: for A being Ordinal
for L being T-Sequence st A = a & L = b holds
( dom L = A & ( for B being Ordinal st B in A holds
L . B = F2((L | B)) ) ) and
 a is Ordinal and
A7: c is T-Sequence and
A8: for A being Ordinal
for L being T-Sequence st A = a & L = c holds
( dom L = A & ( for B being Ordinal st B in A holds
L . B = F2((L | B)) ) ) ; ::_thesis: b = c
reconsider c = c as T-Sequence by A7;
reconsider a = a as Ordinal by A4;
A9: ( dom c = a & ( for B being Ordinal
for L being T-Sequence st B in a & L = c | B holds
c . B = F2(L) ) ) by A8;
reconsider b = b as T-Sequence by A5;
A10: ( dom b = a & ( for B being Ordinal
for L being T-Sequence st B in a & L = b | B holds
b . B = F2(L) ) ) by A6;
 b = c from ORDINAL1:sch_3(A10, A9);
hence  b = c ; ::_thesis: verum
end;
consider G being Function such that
A11: for a, b being set holds
( [a,b] in G iff ( a in B & S2[a,b] ) ) from FUNCT_1:sch_1(A3);
defpred S3[ set , set ] means  ex L being T-Sequence st
( L = G . $1 & $2 = F2(L) );
A12: dom G = B
proof
thus  for a being set st a in dom G holds
a in B :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: B c= dom G
proof
let a be set ; ::_thesis: ( a in dom G implies a in B )
assume  a in dom G ; ::_thesis: a in B
then  ex b being set st [a,b] in G by XTUPLE_0:def_12;
hence  a in B by A11; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B or a in dom G )
assume A13: a in B ; ::_thesis: a in dom G
then reconsider a9 = a as Ordinal by Th13;
consider L being T-Sequence such that
A14: ( dom L = a9 & ( for D being Ordinal st D in a9 holds
L . D = F2((L | D)) ) ) by A2, A13;
 for A being Ordinal
for K being T-Sequence st A = a9 & K = L holds
( dom K = A & ( for B being Ordinal st B in A holds
K . B = F2((K | B)) ) ) by A14;
then  [a9,L] in G by A11, A13;
hence  a in dom G by XTUPLE_0:def_12; ::_thesis: verum
end;
A15: for a being set st a in B holds
ex b being set st S3[a,b]
proof
let a be set ; ::_thesis: ( a in B implies ex b being set st S3[a,b] )
assume  a in B ; ::_thesis: ex b being set st S3[a,b]
then consider c being set  such that
A16: [a,c] in G by A12, XTUPLE_0:def_12;
reconsider L = c as T-Sequence by A11, A16;
take  F2(L) ; ::_thesis: S3[a,F2(L)]
take  L ; ::_thesis: ( L = G . a & F2(L) = F2(L) )
thus  L = G . a by A16, FUNCT_1:1; ::_thesis: F2(L) = F2(L)
thus  F2(L) = F2(L) ; ::_thesis: verum
end;
A17: for a, b, c being set st a in B & S3[a,b] & S3[a,c] holds
b = c ;
consider F being Function such that
A18: ( dom F = B & ( for a being set st a in B holds
S3[a,F . a] ) ) from FUNCT_1:sch_2(A17, A15);
reconsider L = F as T-Sequence by A18, Def7;
take  L ; ::_thesis: ( dom L = B & ( for B being Ordinal st B in B holds
L . B = F2((L | B)) ) )
thus  dom L = B by A18; ::_thesis: for B being Ordinal st B in B holds
L . B = F2((L | B))
let D be Ordinal; ::_thesis: ( D in B implies L . D = F2((L | D)) )
assume A19: D in B ; ::_thesis: L . D = F2((L | D))
then consider K being T-Sequence such that
A20: K = G . D and
A21: F . D = F2(K) by A18;
A22: [D,K] in G by A12, A19, A20, FUNCT_1:1;
then A23: dom K = D by A11;
A24: now__::_thesis:_for_C_being_Ordinal_st_C_in_D_holds_
G_._C_=_K_|_C
let C be Ordinal; ::_thesis: ( C in D implies G . C = K | C )
assume A25: C in D ; ::_thesis: G . C = K | C
A26: now__::_thesis:_for_A_being_Ordinal
for_L_being_T-Sequence_st_A_=_C_&_L_=_K_|_C_holds_
(_dom_L_=_A_&_(_for_B_being_Ordinal_st_B_in_A_holds_
L_._B_=_F2((L_|_B))_)_)
let A be Ordinal; ::_thesis: for L being T-Sequence st A = C & L = K | C holds
( dom L = A & ( for B being Ordinal st B in A holds
L . B = F2((L | B)) ) )
let L be T-Sequence; ::_thesis: ( A = C & L = K | C implies ( dom L = A & ( for B being Ordinal st B in A holds
L . B = F2((L | B)) ) ) )
assume that
A27: A = C and
A28: L = K | C ; ::_thesis: ( dom L = A & ( for B being Ordinal st B in A holds
L . B = F2((L | B)) ) )
A29: C c= D by A25, Def2;
hence A30: dom L = A by A23, A27, A28, RELAT_1:62; ::_thesis: for B being Ordinal st B in A holds
L . B = F2((L | B))
let B be Ordinal; ::_thesis: ( B in A implies L . B = F2((L | B)) )
assume A31: B in A ; ::_thesis: L . B = F2((L | B))
then  B c= A by Def2;
then A32: K | B = L | B by A27, A28, FUNCT_1:51;
 K . B = F2((K | B)) by A11, A22, A27, A29, A31;
hence  L . B = F2((L | B)) by A28, A30, A31, A32, FUNCT_1:47; ::_thesis: verum
end;
 C in B by A19, A25, Th10;
then  [C,(K | C)] in G by A11, A26;
hence  G . C = K | C by FUNCT_1:1; ::_thesis: verum
end;
A33: now__::_thesis:_for_a_being_set_st_a_in_D_holds_
(L_|_D)_._a_=_K_._a
let a be set ; ::_thesis: ( a in D implies (L | D) . a = K . a )
assume A34: a in D ; ::_thesis: (L | D) . a = K . a
then reconsider A = a as Ordinal by Th13;
A35: ( G . A = K | A & (L | D) . A = L . A ) by A24, A34, FUNCT_1:49;
 ex J being T-Sequence st
( J = G . A & F . A = F2(J) ) by A18, A19, A34, Th10;
hence  (L | D) . a = K . a by A11, A22, A34, A35; ::_thesis: verum
end;
 D c= dom L by A18, A19, Def2;
then  dom (L | D) = D by RELAT_1:62;
hence  L . D = F2((L | D)) by A21, A23, A33, FUNCT_1:2; ::_thesis: verum
end;
 for A being Ordinal holds S1[A] from ORDINAL1:sch_2(A1);
then consider L being T-Sequence such that
A36: dom L = F1() and
A37: for B being Ordinal st B in F1() holds
L . B = F2((L | B)) ;
take  L ; ::_thesis: ( dom L = F1() & ( for B being Ordinal
for L1 being T-Sequence st B in F1() & L1 = L | B holds
L . B = F2(L1) ) )
thus  dom L = F1() by A36; ::_thesis: for B being Ordinal
for L1 being T-Sequence st B in F1() & L1 = L | B holds
L . B = F2(L1)
let B be Ordinal; ::_thesis: for L1 being T-Sequence st B in F1() & L1 = L | B holds
L . B = F2(L1)
let L1 be T-Sequence; ::_thesis: ( B in F1() & L1 = L | B implies L . B = F2(L1) )
assume  ( B in F1() & L1 = L | B ) ; ::_thesis: L . B = F2(L1)
hence  L . B = F2(L1) by A37; ::_thesis: verum
end;

scheme :: ORDINAL1:sch 5
FuncTS{ F1() ->  T-Sequence, F2( Ordinal) ->  set , F3( T-Sequence) ->  set } :
 for B being Ordinal st B in dom F1() holds
F1() . B = F3((F1() | B))
provided
A1: for A being Ordinal
for a being set holds
( a = F2(A) iff ex L being T-Sequence st
( a = F3(L) & dom L = A & ( for B being Ordinal st B in A holds
L . B = F3((L | B)) ) ) ) and
A2: for A being Ordinal st A in dom F1() holds
F1() . A = F2(A)
proof
consider L being T-Sequence such that
 F2((dom F1())) = F3(L) and
A3: dom L = dom F1() and
A4: for B being Ordinal st B in dom F1() holds
L . B = F3((L | B)) by A1;
now__::_thesis:_for_b_being_set_st_b_in_dom_L_holds_
F1()_._b_=_L_._b
let b be set ; ::_thesis: ( b in dom L implies F1() . b = L . b )
assume A5: b in dom L ; ::_thesis: F1() . b = L . b
then reconsider B = b as Ordinal by Th13;
now__::_thesis:_ex_K_being_number_st_
(_F3((L_|_B))_=_F3(K)_&_dom_K_=_B_&_(_for_C_being_Ordinal_st_C_in_B_holds_
K_._C_=_F3((K_|_C))_)_)
take K = L | B; ::_thesis: ( F3((L | B)) = F3(K) & dom K = B & ( for C being Ordinal st C in B holds
K . C = F3((K | C)) ) )
thus  F3((L | B)) = F3(K) ; ::_thesis: ( dom K = B & ( for C being Ordinal st C in B holds
K . C = F3((K | C)) ) )
A6: B c= dom L by A5, Def2;
hence  dom K = B by RELAT_1:62; ::_thesis: for C being Ordinal st C in B holds
K . C = F3((K | C))
let C be Ordinal; ::_thesis: ( C in B implies K . C = F3((K | C)) )
assume A7: C in B ; ::_thesis: K . C = F3((K | C))
then  C c= B by Def2;
then A8: L | C = K | C by FUNCT_1:51;
 K . C = L . C by A7, FUNCT_1:49;
hence  K . C = F3((K | C)) by A3, A4, A6, A7, A8; ::_thesis: verum
end;
then F2(B) = F3((L | B)) by A1
.= L . B by A3, A4, A5 ;
hence  F1() . b = L . b by A2, A3, A5; ::_thesis: verum
end;
then  F1() = L by A3, FUNCT_1:2;
hence  for B being Ordinal st B in dom F1() holds
F1() . B = F3((F1() | B)) by A4; ::_thesis: verum
end;

theorem :: ORDINAL1:35
for A, B being Ordinal holds
( A c< B or A = B or B c< A )
proof
let A, B be Ordinal; ::_thesis: ( A c< B or A = B or B c< A )
assume that
A1: ( not A c< B & not A = B ) and
A2: not B c< A ; ::_thesis: contradiction
 not A c= B by A1, XBOOLE_0:def_8;
hence  contradiction by A2, XBOOLE_0:def_8; ::_thesis: verum
end;

begin

definition
let X be set ;
func On X ->  set  means :Def9: :: ORDINAL1:def 9
 for x being set holds
( x in it iff ( x in X & x is Ordinal ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x in X & x is Ordinal ) )
proof
defpred S1[ set ] means $1 is Ordinal;
thus  ex Y being set st
for x being set holds
( x in Y iff ( x in X & S1[x] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in X & x is Ordinal ) ) ) & ( for x being set holds
( x in b2 iff ( x in X & x is Ordinal ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ( $1 in X & $1 is Ordinal );
let Y, Z be set ; ::_thesis: ( ( for x being set holds
( x in Y iff ( x in X & x is Ordinal ) ) ) & ( for x being set holds
( x in Z iff ( x in X & x is Ordinal ) ) ) implies Y = Z )
assume that
A1: for x being set holds
( x in Y iff S1[x] ) and
A2: for x being set holds
( x in Z iff S1[x] ) ; ::_thesis: Y = Z
thus  Y = Z from XBOOLE_0:sch_2(A1, A2); ::_thesis: verum
end;
func Lim X ->  set  means :: ORDINAL1:def 10
 for x being set holds
( x in it iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) )
proof
defpred S1[ set ] means  ex A being Ordinal st
( $1 = A & A is limit_ordinal );
thus  ex Y being set st
for x being set holds
( x in Y iff ( x in X & S1[x] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) ) ) & ( for x being set holds
( x in b2 iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ( $1 in X & ex A being Ordinal st
( $1 = A & A is limit_ordinal ) );
let Y, Z be set ; ::_thesis: ( ( for x being set holds
( x in Y iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) ) ) & ( for x being set holds
( x in Z iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) ) ) implies Y = Z )
assume that
A3: for x being set holds
( x in Y iff S1[x] ) and
A4: for x being set holds
( x in Z iff S1[x] ) ; ::_thesis: Y = Z
thus  Y = Z from XBOOLE_0:sch_2(A3, A4); ::_thesis: verum
end;
end;

:: deftheorem Def9 defines On ORDINAL1:def_9_:_
 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_10_:_
 for X, b2 being set holds
( b2 = Lim X iff for x being set holds
( x in b2 iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) ) );

theorem Th36: :: ORDINAL1:36
for D being Ordinal ex A being Ordinal st
( D in A & A is limit_ordinal )
proof
let D be Ordinal; ::_thesis: ex A being Ordinal st
( D in A & A is limit_ordinal )
consider Field being set  such that
A1: D in Field and
A2: for X, Y being set st X in Field & Y c= X holds
Y in Field and
A3: for X being set st X in Field holds
bool X in Field and
 for X being set holds
( not X c= Field or X,Field are_equipotent or X in Field ) by ZFMISC_1:112;
 for X being set st X in On Field holds
( X is Ordinal & X c= On Field )
proof
let X be set ; ::_thesis: ( X in On Field implies ( X is Ordinal & X c= On Field ) )
assume A4: X in On Field ; ::_thesis: ( X is Ordinal & X c= On Field )
then reconsider A = X as Ordinal by Def9;
A5: A in Field by A4, Def9;
thus  X is Ordinal by A4, Def9; ::_thesis: X c= On Field
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X or y in On Field )
assume A6: y in X ; ::_thesis: y in On Field
then  y in A ;
then reconsider B = y as Ordinal by Th13;
 B c= A by A6, Def2;
then  B in Field by A2, A5;
hence  y in On Field by Def9; ::_thesis: verum
end;
then reconsider ON = On Field as Ordinal by Th19;
take  ON ; ::_thesis: ( D in ON & ON is limit_ordinal )
thus  D in ON by A1, Def9; ::_thesis: ON is limit_ordinal
 for A being Ordinal st A in ON holds
succ A in ON
proof
let A be Ordinal; ::_thesis: ( A in ON implies succ A in ON )
A7: succ A c= bool A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in succ A or x in bool A )
assume  x in succ A ; ::_thesis: x in bool A
then  ( x in A or x = A ) by Th8;
then  x c= A by Def2;
hence  x in bool A ; ::_thesis: verum
end;
assume  A in ON ; ::_thesis: succ A in ON
then  A in Field by Def9;
then  bool A in Field by A3;
then  succ A in Field by A2, A7;
hence  succ A in ON by Def9; ::_thesis: verum
end;
hence  ON is limit_ordinal by Th28; ::_thesis: verum
end;

definition
func omega  ->  set  means :Def11: :: ORDINAL1:def 11
( {} in it & it is limit_ordinal & it is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
it c= A ) );
existence
 ex b1 being set st
( {} in b1 & b1 is limit_ordinal & b1 is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
b1 c= A ) )
proof
defpred S1[ Ordinal] means ( {} in $1 & $1 is limit_ordinal );
A1: ex A being Ordinal st S1[A] by Th36;
 ex C being Ordinal st
( S1[C] & ( for A being Ordinal st S1[A] holds
C c= A ) ) from ORDINAL1:sch_1(A1);
hence  ex b1 being set st
( {} in b1 & b1 is limit_ordinal & b1 is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
b1 c= A ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st {} in b1 & b1 is limit_ordinal & b1 is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
b1 c= A ) & {} in b2 & b2 is limit_ordinal & b2 is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
b2 c= A ) holds
b1 = b2
proof
let B, C be set ; ::_thesis: ( {} in B & B is limit_ordinal & B is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
B c= A ) & {} in C & C is limit_ordinal & C is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
C c= A ) implies B = C )
assume  ( {} in B & B is limit_ordinal & B is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
B c= A ) & {} in C & C is limit_ordinal & C is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
C c= A ) ) ; ::_thesis: B = C
hence  ( B c= C & C c= B ) ; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
end;

:: deftheorem Def11 defines omega ORDINAL1:def_11_:_
 for b1 being set holds
( b1 = omega iff ( {} in b1 & b1 is limit_ordinal & b1 is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
b1 c= A ) ) );

registration
cluster omega  ->  non empty ordinal ;
coherence
 ( not omega is empty & omega is ordinal ) by Def11;
end;

definition
let A be set ;
attrA is natural  means :Def12: :: ORDINAL1:def 12
A in omega ;
end;

:: deftheorem Def12 defines natural ORDINAL1:def_12_:_
 for A being set holds
( A is natural iff A in omega );

registration
cluster natural for number ;
existence
 ex b1 being number st b1 is natural
proof
take n = the Element of omega ; ::_thesis: n is natural
thus  n in omega ; :: according to ORDINAL1:def_12 ::_thesis: verum
end;
end;

definition
mode Nat is natural number ;
end;

registration
natural number  ex b1 being number st
for b2 being natural number holds b2 in b1
proof
take  omega ; ::_thesis: for b1 being natural number holds b1 in omega
let y be Nat; ::_thesis: y in omega
thus  y in omega by Def12; ::_thesis: verum
end;
end;

registration
let A be Ordinal;
cluster  ->  ordinal for Element of A;
coherence
 for b1 being Element of A holds b1 is ordinal
proof
let x be Element of A; ::_thesis: x is ordinal
 ( A is empty or not A is empty ) ;
hence  x is ordinal by Th13, SUBSET_1:def_1; ::_thesis: verum
end;
end;

registration
cluster natural  ->  ordinal for number ;
coherence
 for b1 being number st b1 is natural holds
b1 is ordinal
proof
let n be number ; ::_thesis: ( n is natural implies n is ordinal )
assume  n is natural ; ::_thesis: n is ordinal
then reconsider n = n as Element of omega by Def12;
 n is ordinal ;
hence  n is ordinal ; ::_thesis: verum
end;
end;

scheme :: ORDINAL1:sch 6
ALFA{ F1() ->  non empty set , P1[ set , set ] } :
 ex F being Function st
( dom F = F1() & ( for d being Element of F1() ex A being Ordinal st
( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds
A c= B ) ) ) )
provided
A1: for d being Element of F1() ex A being Ordinal st P1[d,A]
proof
defpred S1[ set , set ] means  ex A being Ordinal st
( A = $2 & P1[$1,A] & ( for B being Ordinal st P1[$1,B] holds
A c= B ) );
A2: for x being set st x in F1() holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in F1() implies ex y being set st S1[x,y] )
assume  x in F1() ; ::_thesis: ex y being set st S1[x,y]
then reconsider d = x as Element of F1() ;
defpred S2[ Ordinal] means P1[d,$1];
A3: ex A being Ordinal st S2[A] by A1;
consider A being Ordinal such that
A4: ( S2[A] & ( for B being Ordinal st S2[B] holds
A c= B ) ) from ORDINAL1:sch_1(A3);
reconsider y = A as set ;
take  y ; ::_thesis: S1[x,y]
take  A ; ::_thesis: ( A = y & P1[x,A] & ( for B being Ordinal st P1[x,B] holds
A c= B ) )
thus  ( A = y & P1[x,A] & ( for B being Ordinal st P1[x,B] holds
A c= B ) ) by A4; ::_thesis: verum
end;
A5: for x, y, z being set st x in F1() & S1[x,y] & S1[x,z] holds
y = z
proof
let x, y, z be set ; ::_thesis: ( x in F1() & S1[x,y] & S1[x,z] implies y = z )
assume  x in F1() ; ::_thesis: ( not S1[x,y] or not S1[x,z] or y = z )
given A1 being Ordinal such that A6: A1 = y and
A7: ( P1[x,A1] & ( for B being Ordinal st P1[x,B] holds
A1 c= B ) ) ; ::_thesis: ( not S1[x,z] or y = z )
given A2 being Ordinal such that A8: A2 = z and
A9: ( P1[x,A2] & ( for B being Ordinal st P1[x,B] holds
A2 c= B ) ) ; ::_thesis: y = z
 ( A1 c= A2 & A2 c= A1 ) by A7, A9;
hence  y = z by A6, A8, XBOOLE_0:def_10; ::_thesis: verum
end;
consider F being Function such that
A10: ( dom F = F1() & ( for x being set st x in F1() holds
S1[x,F . x] ) ) from FUNCT_1:sch_2(A5, A2);
take  F ; ::_thesis: ( dom F = F1() & ( for d being Element of F1() ex A being Ordinal st
( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds
A c= B ) ) ) )
thus  dom F = F1() by A10; ::_thesis: for d being Element of F1() ex A being Ordinal st
( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds
A c= B ) )
let d be Element of F1(); ::_thesis: ex A being Ordinal st
( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds
A c= B ) )
thus  ex A being Ordinal st
( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds
A c= B ) ) by A10; ::_thesis: verum
end;

theorem :: ORDINAL1:37
for X being set holds (succ X) \ {X} = X
proof
let X be set ; ::_thesis: (succ X) \ {X} = X
thus  (succ X) \ {X} c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= (succ X) \ {X}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (succ X) \ {X} or x in X )
assume A1: x in (succ X) \ {X} ; ::_thesis: x in X
then A2: not x in {X} by XBOOLE_0:def_5;
 ( x in X or x = X ) by A1, Th8;
hence  x in X by A2, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (succ X) \ {X} )
assume A3: x in X ; ::_thesis: x in (succ X) \ {X}
then  x <> X ;
then A4: not x in {X} by TARSKI:def_1;
 x in succ X by A3, Th8;
hence  x in (succ X) \ {X} by A4, XBOOLE_0:def_5; ::_thesis: verum
end;

registration
cluster empty  ->  natural for number ;
coherence
 for b1 being number st b1 is empty holds
b1 is natural
proof
 {} in omega by Def11;
hence  for b1 being number st b1 is empty holds
b1 is natural by Def12; ::_thesis: verum
end;
cluster  ->  natural for Element of omega ;
coherence
 for b1 being Element of omega holds b1 is natural by Def12;
end;

registration
cluster non empty natural for number ;
existence
 ex b1 being number st
( not b1 is empty & b1 is natural )
proof
take  succ {} ; ::_thesis: ( not succ {} is empty & succ {} is natural )
thus  not succ {} is empty ; ::_thesis: succ {} is natural
 ( omega is limit_ordinal & {} in omega ) by Def11;
hence  succ {} in omega by Th28; :: according to ORDINAL1:def_12 ::_thesis: verum
end;
end;

registration
let a be natural Ordinal;
cluster succ a ->  natural ;
coherence
 succ a is natural
proof
 ( omega is limit_ordinal & a in omega ) by Def11, Def12;
hence  succ a in omega by Th28; :: according to ORDINAL1:def_12 ::_thesis: verum
end;
end;

registration
cluster empty  ->  c=-linear for number ;
coherence
 for b1 being set st b1 is empty holds
b1 is c=-linear
proof
let X be set ; ::_thesis: ( X is empty implies X is c=-linear )
assume A1: X is empty ; ::_thesis: X is c=-linear
let x be set ; :: according to ORDINAL1:def_8 ::_thesis: for y being set st x in X & y in X holds
x,y are_c=-comparable
thus  for y being set st x in X & y in X holds
x,y are_c=-comparable by A1; ::_thesis: verum
end;
end;

registration
let X be c=-linear set ;
cluster  ->  c=-linear for Element of bool X;
coherence
 for b1 being Subset of X holds b1 is c=-linear
proof
let Y be Subset of X; ::_thesis: Y is c=-linear
let x, y be set ; :: according to ORDINAL1:def_8 ::_thesis: ( x in Y & y in Y implies x,y are_c=-comparable )
assume  ( x in Y & y in Y ) ; ::_thesis: x,y are_c=-comparable
hence  x,y are_c=-comparable by Def8; ::_thesis: verum
end;
end;