:: CLASSES2 semantic presentation

begin

            Lm1:  for X being set holds Tarski-Class X is Tarski
proof
let X be set ; ::_thesis: Tarski-Class X is Tarski
 Tarski-Class X is_Tarski-Class_of X by CLASSES1:def_4;
hence  Tarski-Class X is Tarski by CLASSES1:def_3; ::_thesis: verum
end;

registration
cluster Tarski  ->  subset-closed for set ;
coherence
 for b1 being set st b1 is Tarski holds
b1 is subset-closed by CLASSES1:def_2;
end;

registration
let X be set ;
cluster Tarski-Class X ->  Tarski ;
coherence
 Tarski-Class X is Tarski by Lm1;
end;

theorem Th1: :: CLASSES2:1
for W, X being set st W is subset-closed & X in W holds
( not X,W are_equipotent & card X in card W )
proof
let W, X be set ; ::_thesis: ( W is subset-closed & X in W implies ( not X,W are_equipotent & card X in card W ) )
assume A1: W is subset-closed ; ::_thesis: ( not X in W or ( not X,W are_equipotent & card X in card W ) )
assume A2: X in W ; ::_thesis: ( not X,W are_equipotent & card X in card W )
 bool X c= W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in bool X or x in W )
assume  x in bool X ; ::_thesis: x in W
hence  x in W by A1, A2, CLASSES1:def_1; ::_thesis: verum
end;
then A3: card (bool X) c= card W by CARD_1:11;
A4: card X in card (bool X) by CARD_1:14;
then  card X in card W by A3;
then  card X <> card W ;
hence  ( not X,W are_equipotent & card X in card W ) by A4, A3, CARD_1:5; ::_thesis: verum
end;

theorem Th2: :: CLASSES2:2
for W, x, y being set st W is Tarski & x in W & y in W holds
( {x} in W & {x,y} in W )
proof
let W, x, y be set ; ::_thesis: ( W is Tarski & x in W & y in W implies ( {x} in W & {x,y} in W ) )
defpred S1[ set ] means $1 = {} ;
assume that
A1: W is Tarski and
A2: x in W and
A3: y in W ; ::_thesis: ( {x} in W & {x,y} in W )
A4: {x} c= bool x by ZFMISC_1:68;
 bool x in W by A1, A2, CLASSES1:def_2;
hence  {x} in W by A1, A4, CLASSES1:def_1; ::_thesis: {x,y} in W
then A5: bool {x} in W by A1, CLASSES1:def_2;
deffunc H1( set ) ->  set = x;
deffunc H2( set ) ->  set = y;
consider f being Function such that
A6: ( dom f = {{},{x}} & ( for z being set st z in {{},{x}} holds
( ( S1[z] implies f . z = H2(z) ) & ( not S1[z] implies f . z = H1(z) ) ) ) ) from PARTFUN1:sch_1();
 {x,y} c= rng f
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x,y} or z in rng f )
A7: {} in {{},{x}} by TARSKI:def_2;
A8: {x} in {{},{x}} by TARSKI:def_2;
assume  z in {x,y} ; ::_thesis: z in rng f
then  ( z = x or z = y ) by TARSKI:def_2;
then  ( f . {} = z or f . {x} = z ) by A6, A7, A8;
hence  z in rng f by A6, A7, A8, FUNCT_1:def_3; ::_thesis: verum
end;
then A9: card {x,y} c= card {{},{x}} by A6, CARD_1:12;
A10: {x,y} c= W
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x,y} or z in W )
assume  z in {x,y} ; ::_thesis: z in W
hence  z in W by A2, A3, TARSKI:def_2; ::_thesis: verum
end;
 bool {x} = {{},{x}} by ZFMISC_1:24;
then  card {{},{x}} in card W by A1, A5, Th1;
then  card {x,y} in card W by A9, ORDINAL1:12;
hence  {x,y} in W by A1, A10, CLASSES1:1; ::_thesis: verum
end;

theorem Th3: :: CLASSES2:3
for W, x, y being set st W is Tarski & x in W & y in W holds
[x,y] in W
proof
let W, x, y be set ; ::_thesis: ( W is Tarski & x in W & y in W implies [x,y] in W )
assume A1: W is Tarski ; ::_thesis: ( not x in W or not y in W or [x,y] in W )
assume that
A2: x in W and
A3: y in W ; ::_thesis: [x,y] in W
A4: {x} in W by A1, A2, Th2;
 {x,y} in W by A1, A2, A3, Th2;
hence  [x,y] in W by A1, A4, Th2; ::_thesis: verum
end;

theorem Th4: :: CLASSES2:4
for W, X being set st W is Tarski & X in W holds
Tarski-Class X c= W
proof
let W, X be set ; ::_thesis: ( W is Tarski & X in W implies Tarski-Class X c= W )
assume that
A1: W is Tarski and
A2: X in W ; ::_thesis: Tarski-Class X c= W
reconsider D = W as non empty set by A2;
 D is_Tarski-Class_of X by A1, A2, CLASSES1:def_3;
hence  Tarski-Class X c= W by CLASSES1:def_4; ::_thesis: verum
end;

theorem Th5: :: CLASSES2:5
for A being Ordinal
for W being set st W is Tarski & A in W holds
( succ A in W & A c= W )
proof
let A be Ordinal; ::_thesis: for W being set st W is Tarski & A in W holds
( succ A in W & A c= W )
let W be set ; ::_thesis: ( W is Tarski & A in W implies ( succ A in W & A c= W ) )
assume that
A1: for X, Y being set st X in W & Y c= X holds
Y in W and
A2: for X being set st X in W holds
bool X in W and
 for X being set holds
( not X c= W or X,W are_equipotent or X in W ) and
A3: A in W ; :: according to CLASSES1:def_1,CLASSES1:def_2 ::_thesis: ( succ A in W & A c= W )
 bool A in W by A2, A3;
hence  succ A in W by A1, ORDINAL2:3; ::_thesis: A c= W
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in W )
assume A4: x in A ; ::_thesis: x in W
then reconsider B = x as Ordinal ;
 B c= A by A4, ORDINAL1:def_2;
hence  x in W by A1, A3; ::_thesis: verum
end;

theorem :: CLASSES2:6
for A being Ordinal
for W being set st A in Tarski-Class W holds
( succ A in Tarski-Class W & A c= Tarski-Class W ) by Th5;

theorem Th7: :: CLASSES2:7
for W, X being set st W is subset-closed & X is epsilon-transitive & X in W holds
X c= W
proof
let W, X be set ; ::_thesis: ( W is subset-closed & X is epsilon-transitive & X in W implies X c= W )
assume that
A1: for X, Y being set st X in W & Y c= X holds
Y in W and
A2: for Y being set st Y in X holds
Y c= X and
A3: X in W ; :: according to ORDINAL1:def_2,CLASSES1:def_1 ::_thesis: X c= W
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in W )
thus  ( not x in X or x in W ) by A1, A2, A3; ::_thesis: verum
end;

theorem :: CLASSES2:8
for X, W being set st X is epsilon-transitive & X in Tarski-Class W holds
X c= Tarski-Class W by Th7;

theorem Th9: :: CLASSES2:9
for W being set st W is Tarski holds
On W = card W
proof
let W be set ; ::_thesis: ( W is Tarski implies On W = card W )
assume A1: W is Tarski ; ::_thesis: On W = card W
now__::_thesis:_for_X_being_set_st_X_in_On_W_holds_
(_X_is_Ordinal_&_X_c=_On_W_)
let X be set ; ::_thesis: ( X in On W implies ( X is Ordinal & X c= On W ) )
assume A2: X in On W ; ::_thesis: ( X is Ordinal & X c= On W )
hence  X is Ordinal by ORDINAL1:def_9; ::_thesis: X c= On W
reconsider A = X as Ordinal by A2, ORDINAL1:def_9;
A3: X in W by A2, ORDINAL1:def_9;
thus  X c= On W ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in On W )
assume A4: x in X ; ::_thesis: x in On W
then  x in A ;
then reconsider B = x as Ordinal ;
 B c= A by A4, ORDINAL1:def_2;
then  B in W by A1, A3, CLASSES1:def_1;
hence  x in On W by ORDINAL1:def_9; ::_thesis: verum
end;
end;
then reconsider ON = On W as Ordinal by ORDINAL1:19;
A5: now__::_thesis:_not_ON_in_W
assume  ON in W ; ::_thesis: contradiction
then  ON in ON by ORDINAL1:def_9;
hence  contradiction ; ::_thesis: verum
end;
 ON c= W by ORDINAL2:7;
then A6: ( ON,W are_equipotent or ON in W ) by A1, CLASSES1:def_2;
now__::_thesis:_for_A_being_Ordinal_st_A,ON_are_equipotent_holds_
ON_c=_A
let A be Ordinal; ::_thesis: ( A,ON are_equipotent implies ON c= A )
assume that
A7: A,ON are_equipotent and
A8: not ON c= A ; ::_thesis: contradiction
 A in ON by A8, ORDINAL1:16;
then  A in W by ORDINAL1:def_9;
hence  contradiction by A1, A6, A5, A7, Th1, WELLORD2:15; ::_thesis: verum
end;
then reconsider ON = ON as Cardinal by CARD_1:def_1;
 ON = card ON by CARD_1:def_2;
hence  On W = card W by A6, A5, CARD_1:5; ::_thesis: verum
end;

theorem :: CLASSES2:10
for W being set holds On (Tarski-Class W) = card (Tarski-Class W) by Th9;

theorem Th11: :: CLASSES2:11
for W, X being set st W is Tarski & X in W holds
card X in W
proof
let W, X be set ; ::_thesis: ( W is Tarski & X in W implies card X in W )
assume that
A1: W is Tarski and
A2: X in W ; ::_thesis: card X in W
A3: card W = On W by A1, Th9;
 card X in card W by A1, A2, Th1;
hence  card X in W by A3, ORDINAL1:def_9; ::_thesis: verum
end;

theorem :: CLASSES2:12
for X, W being set st X in Tarski-Class W holds
card X in Tarski-Class W by Th11;

theorem Th13: :: CLASSES2:13
for W, x being set st W is Tarski & x in card W holds
x in W
proof
let W, x be set ; ::_thesis: ( W is Tarski & x in card W implies x in W )
assume A1: W is Tarski ; ::_thesis: ( not x in card W or x in W )
assume  x in card W ; ::_thesis: x in W
then  x in On W by A1, Th9;
hence  x in W by ORDINAL1:def_9; ::_thesis: verum
end;

theorem :: CLASSES2:14
for x, W being set st x in card (Tarski-Class W) holds
x in Tarski-Class W by Th13;

theorem :: CLASSES2:15
for m being Cardinal
for W being set st W is Tarski & m in card W holds
m in W
proof
let m be Cardinal; ::_thesis: for W being set st W is Tarski & m in card W holds
m in W
let W be set ; ::_thesis: ( W is Tarski & m in card W implies m in W )
assume A1: W is Tarski ; ::_thesis: ( not m in card W or m in W )
assume  m in card W ; ::_thesis: m in W
then  m in On W by A1, Th9;
hence  m in W by ORDINAL1:def_9; ::_thesis: verum
end;

theorem :: CLASSES2:16
for m being Cardinal
for W being set st m in card (Tarski-Class W) holds
m in Tarski-Class W
proof
let m be Cardinal; ::_thesis: for W being set st m in card (Tarski-Class W) holds
m in Tarski-Class W
let W be set ; ::_thesis: ( m in card (Tarski-Class W) implies m in Tarski-Class W )
assume  m in card (Tarski-Class W) ; ::_thesis: m in Tarski-Class W
then  m in On (Tarski-Class W) by Th9;
hence  m in Tarski-Class W by ORDINAL1:def_9; ::_thesis: verum
end;

theorem :: CLASSES2:17
for m being Cardinal
for W being set st W is Tarski & m in W holds
m c= W by Th5;

theorem :: CLASSES2:18
for m being Cardinal
for W being set st m in Tarski-Class W holds
m c= Tarski-Class W by Th5;

theorem Th19: :: CLASSES2:19
for W being set st W is Tarski holds
card W is limit_ordinal
proof
let W be set ; ::_thesis: ( W is Tarski implies card W is limit_ordinal )
assume A1: W is Tarski ; ::_thesis: card W is limit_ordinal
now__::_thesis:_for_A_being_Ordinal_st_A_in_card_W_holds_
succ_A_in_card_W
let A be Ordinal; ::_thesis: ( A in card W implies succ A in card W )
assume  A in card W ; ::_thesis: succ A in card W
then  A in W by A1, Th13;
then  succ A in W by A1, Th5;
then  succ A in On W by ORDINAL1:def_9;
hence  succ A in card W by A1, Th9; ::_thesis: verum
end;
hence  card W is limit_ordinal by ORDINAL1:28; ::_thesis: verum
end;

theorem :: CLASSES2:20
for W being set st W is Tarski & W <> {} holds
( card W <> 0 & card W <> {} & card W is limit_ordinal ) by Th19;

theorem Th21: :: CLASSES2:21
for W being set holds
( card (Tarski-Class W) <> 0 & card (Tarski-Class W) <> {} & card (Tarski-Class W) is limit_ordinal )
proof
let W be set ; ::_thesis: ( card (Tarski-Class W) <> 0 & card (Tarski-Class W) <> {} & card (Tarski-Class W) is limit_ordinal )
thus  card (Tarski-Class W) <> 0 ; ::_thesis: ( card (Tarski-Class W) <> {} & card (Tarski-Class W) is limit_ordinal )
thus  card (Tarski-Class W) <> {} ; ::_thesis: card (Tarski-Class W) is limit_ordinal
now__::_thesis:_for_A_being_Ordinal_st_A_in_card_(Tarski-Class_W)_holds_
succ_A_in_card_(Tarski-Class_W)
let A be Ordinal; ::_thesis: ( A in card (Tarski-Class W) implies succ A in card (Tarski-Class W) )
assume  A in card (Tarski-Class W) ; ::_thesis: succ A in card (Tarski-Class W)
then  A in Tarski-Class W by Th13;
then  succ A in Tarski-Class W by Th5;
then  succ A in On (Tarski-Class W) by ORDINAL1:def_9;
hence  succ A in card (Tarski-Class W) by Th9; ::_thesis: verum
end;
hence  card (Tarski-Class W) is limit_ordinal by ORDINAL1:28; ::_thesis: verum
end;


theorem Th22: :: CLASSES2:22
for W, X being set st W is Tarski & ( ( X in W & W is epsilon-transitive ) or ( X in W & X c= W ) or ( card X in card W & X c= W ) ) holds
Funcs (X,W) c= W
proof
let W, X be set ; ::_thesis: ( W is Tarski & ( ( X in W & W is epsilon-transitive ) or ( X in W & X c= W ) or ( card X in card W & X c= W ) ) implies Funcs (X,W) c= W )
assume A1: W is Tarski ; ::_thesis: ( ( not ( X in W & W is epsilon-transitive ) & not ( X in W & X c= W ) & not ( card X in card W & X c= W ) ) or Funcs (X,W) c= W )
assume A2: ( ( X in W & W is epsilon-transitive ) or ( X in W & X c= W ) or ( card X in card W & X c= W ) ) ; ::_thesis: Funcs (X,W) c= W
A3: card X in card W by A1, A2, Th1;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Funcs (X,W) or x in W )
assume A4: x in Funcs (X,W) ; ::_thesis: x in W
then consider f being Function such that
A5: x = f and
A6: dom f = X and
A7: rng f c= W by FUNCT_2:def_2;
A8: X c= W by A2, ORDINAL1:def_2;
A9: f c= W
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f or y in W )
assume A10: y in f ; ::_thesis: y in W
then consider y1, y2 being set  such that
A11: [y1,y2] = y by RELAT_1:def_1;
A12: y1 in dom f by A10, A11, FUNCT_1:1;
 y2 = f . y1 by A10, A11, FUNCT_1:1;
then  y2 in rng f by A12, FUNCT_1:def_3;
hence  y in W by A1, A8, A6, A7, A11, A12, Th3; ::_thesis: verum
end;
 card f = card X by A4, A5, CARD_2:3;
hence  x in W by A1, A3, A5, A9, CLASSES1:1; ::_thesis: verum
end;

theorem :: CLASSES2:23
for X, W being set st ( ( X in Tarski-Class W & W is epsilon-transitive ) or ( X in Tarski-Class W & X c= Tarski-Class W ) or ( card X in card (Tarski-Class W) & X c= Tarski-Class W ) ) holds
Funcs (X,(Tarski-Class W)) c= Tarski-Class W
proof
let X, W be set ; ::_thesis: ( ( ( X in Tarski-Class W & W is epsilon-transitive ) or ( X in Tarski-Class W & X c= Tarski-Class W ) or ( card X in card (Tarski-Class W) & X c= Tarski-Class W ) ) implies Funcs (X,(Tarski-Class W)) c= Tarski-Class W )
assume A1: ( ( X in Tarski-Class W & W is epsilon-transitive ) or ( X in Tarski-Class W & X c= Tarski-Class W ) or ( card X in card (Tarski-Class W) & X c= Tarski-Class W ) ) ; ::_thesis: Funcs (X,(Tarski-Class W)) c= Tarski-Class W
A2: card X in card (Tarski-Class W) by A1, CLASSES1:24;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Funcs (X,(Tarski-Class W)) or x in Tarski-Class W )
assume A3: x in Funcs (X,(Tarski-Class W)) ; ::_thesis: x in Tarski-Class W
then consider f being Function such that
A4: x = f and
A5: dom f = X and
A6: rng f c= Tarski-Class W by FUNCT_2:def_2;
 ( W is epsilon-transitive implies Tarski-Class W is epsilon-transitive ) by CLASSES1:23;
then A7: X c= Tarski-Class W by A1, ORDINAL1:def_2;
A8: f c= Tarski-Class W
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f or y in Tarski-Class W )
assume A9: y in f ; ::_thesis: y in Tarski-Class W
then consider y1, y2 being set  such that
A10: [y1,y2] = y by RELAT_1:def_1;
A11: y1 in dom f by A9, A10, FUNCT_1:1;
 y2 = f . y1 by A9, A10, FUNCT_1:1;
then  y2 in rng f by A11, FUNCT_1:def_3;
hence  y in Tarski-Class W by A7, A5, A6, A10, A11, CLASSES1:27; ::_thesis: verum
end;
 card f = card X by A3, A4, CARD_2:3;
hence  x in Tarski-Class W by A2, A4, A8, CLASSES1:6; ::_thesis: verum
end;

theorem Th24: :: CLASSES2:24
for L being T-Sequence st dom L is limit_ordinal & ( for A being Ordinal st A in dom L holds
L . A = Rank A ) holds
Rank (dom L) = Union L
proof
let L be T-Sequence; ::_thesis: ( dom L is limit_ordinal & ( for A being Ordinal st A in dom L holds
L . A = Rank A ) implies Rank (dom L) = Union L )
assume that
A1: dom L is limit_ordinal and
A2: for A being Ordinal st A in dom L holds
L . A = Rank A ; ::_thesis: Rank (dom L) = Union L
A3: union (rng L) = Union L by CARD_3:def_4;
now__::_thesis:_(_dom_L_<>_{}_implies_(_Rank_(dom_L)_c=_Union_L_&_Union_L_c=_Rank_(dom_L)_)_)
assume A4: dom L <> {} ; ::_thesis: ( Rank (dom L) c= Union L & Union L c= Rank (dom L) )
thus  Rank (dom L) c= Union L ::_thesis: Union L c= Rank (dom L)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Rank (dom L) or x in Union L )
assume  x in Rank (dom L) ; ::_thesis: x in Union L
then consider A being Ordinal such that
A5: A in dom L and
A6: x in Rank A by A1, A4, CLASSES1:31;
 L . A = Rank A by A2, A5;
then  Rank A in rng L by A5, FUNCT_1:def_3;
hence  x in Union L by A3, A6, TARSKI:def_4; ::_thesis: verum
end;
thus  Union L c= Rank (dom L) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union L or x in Rank (dom L) )
assume  x in Union L ; ::_thesis: x in Rank (dom L)
then consider X being set  such that
A7: x in X and
A8: X in rng L by A3, TARSKI:def_4;
consider y being set  such that
A9: y in dom L and
A10: X = L . y by A8, FUNCT_1:def_3;
reconsider y = y as Ordinal by A9;
 X = Rank y by A2, A9, A10;
hence  x in Rank (dom L) by A1, A7, A9, CLASSES1:31; ::_thesis: verum
end;
end;
hence  Rank (dom L) = Union L by A3, CLASSES1:29, RELAT_1:42, XBOOLE_0:def_10, ZFMISC_1:2; ::_thesis: verum
end;

defpred S1[ Ordinal] means  for W being set st W is Tarski & $1 in On W holds
( card (Rank $1) in card W & Rank $1 in W );

Lm2:  S1[ {} ]
by Th9, CARD_1:27, CLASSES1:29, ORDINAL1:def_9;

Lm3:  for A being Ordinal st S1[A] holds
S1[ succ A]
proof
let A be Ordinal; ::_thesis: ( S1[A] implies S1[ succ A] )
assume A1: S1[A] ; ::_thesis: S1[ succ A]
A2: A in succ A by ORDINAL1:6;
let W be set ; ::_thesis: ( W is Tarski & succ A in On W implies ( card (Rank (succ A)) in card W & Rank (succ A) in W ) )
assume that
A3: W is Tarski and
A4: succ A in On W ; ::_thesis: ( card (Rank (succ A)) in card W & Rank (succ A) in W )
 card W = On W by A3, Th9;
then  A in On W by A4, A2, ORDINAL1:10;
then  Rank A in W by A1, A3;
then A5: bool (Rank A) in W by A3, CLASSES1:def_2;
 Rank (succ A) = bool (Rank A) by CLASSES1:30;
hence  ( card (Rank (succ A)) in card W & Rank (succ A) in W ) by A3, A5, Th1; ::_thesis: verum
end;

Lm4:  for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
deffunc H1( Ordinal) ->  set = Rank $1;
assume that
A1: A <> {} and
A2: A is limit_ordinal and
A3: for B being Ordinal st B in A holds
S1[B] ; ::_thesis: S1[A]
let W be set ; ::_thesis: ( W is Tarski & A in On W implies ( card (Rank A) in card W & Rank A in W ) )
assume that
A4: W is Tarski and
A5: A in On W ; ::_thesis: ( card (Rank A) in card W & Rank A in W )
consider L being T-Sequence such that
A6: ( dom L = A & ( for B being Ordinal st B in A holds
L . B = H1(B) ) ) from ORDINAL2:sch_2();
deffunc H2( set ) ->  set = card (bool (L . $1));
consider F being Cardinal-Function such that
A7: ( dom F = A & ( for x being set st x in A holds
F . x = H2(x) ) ) from CARD_3:sch_1();
A8: product F c= Funcs (A,W)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product F or x in Funcs (A,W) )
assume  x in product F ; ::_thesis: x in Funcs (A,W)
then consider f being Function such that
A9: x = f and
A10: dom f = dom F and
A11: for x being set st x in dom F holds
f . x in F . x by CARD_3:def_5;
 rng f c= W
proof
A12: A in W by A5, ORDINAL1:def_9;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in W )
assume  z in rng f ; ::_thesis: z in W
then consider y being set  such that
A13: y in dom f and
A14: z = f . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A7, A10, A13;
A15: f . y in F . y by A10, A11, A13;
 y c= A by A7, A10, A13, ORDINAL1:def_2;
then  y in W by A4, A12, CLASSES1:def_1;
then A16: y in On W by ORDINAL1:def_9;
 L . y = Rank y by A6, A7, A10, A13;
then  L . y in W by A3, A4, A7, A10, A13, A16;
then  bool (L . y) in W by A4, CLASSES1:def_2;
then A17: card (bool (L . y)) in W by A4, Th11;
 F . y = card (bool (L . y)) by A7, A10, A13;
then  F . y c= W by A4, A17, Th5;
hence  z in W by A14, A15; ::_thesis: verum
end;
hence  x in Funcs (A,W) by A7, A9, A10, FUNCT_2:def_2; ::_thesis: verum
end;
A18: Product F = card (product F) by CARD_3:def_8;
A19: A in W by A5, ORDINAL1:def_9;
then  A c= W by A4, Th5;
then  Funcs (A,W) c= W by A4, A19, Th22;
then  product F c= W by A8, XBOOLE_1:1;
then A20: Product F c= card W by A18, CARD_1:11;
A21: for x being set st x in dom (Card L) holds
(Card L) . x in F . x
proof
let x be set ; ::_thesis: ( x in dom (Card L) implies (Card L) . x in F . x )
A22: card (L . x) in card (bool (L . x)) by CARD_1:14;
assume  x in dom (Card L) ; ::_thesis: (Card L) . x in F . x
then A23: x in dom L by CARD_3:def_2;
then  F . x = card (bool (L . x)) by A6, A7;
hence  (Card L) . x in F . x by A23, A22, CARD_3:def_2; ::_thesis: verum
end;
 dom (Card L) = dom L by CARD_3:def_2;
then A24: Sum (Card L) in Product F by A6, A7, A21, CARD_3:41;
A25: Rank A c= W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Rank A or x in W )
assume  x in Rank A ; ::_thesis: x in W
then consider B being Ordinal such that
A26: B in A and
A27: x in Rank B by A1, A2, CLASSES1:31;
 B c= A by A26, ORDINAL1:def_2;
then  B in W by A4, A19, CLASSES1:def_1;
then  B in On W by ORDINAL1:def_9;
then  Rank B c= W by A3, A4, A26, Th7;
hence  x in W by A27; ::_thesis: verum
end;
A28: Rank A = Union L by A2, A6, Th24;
hence  card (Rank A) in card W by A24, A20, CARD_3:39, ORDINAL1:12; ::_thesis: Rank A in W
 card (Rank A) in Product F by A28, A24, CARD_3:39, ORDINAL1:12;
hence  Rank A in W by A4, A20, A25, CLASSES1:1; ::_thesis: verum
end;

theorem Th25: :: CLASSES2:25
for A being Ordinal
for W being set st W is Tarski & A in On W holds
( card (Rank A) in card W & Rank A in W )
proof
let A be Ordinal; ::_thesis: for W being set st W is Tarski & A in On W holds
( card (Rank A) in card W & Rank A in W )
let W be set ; ::_thesis: ( W is Tarski & A in On W implies ( card (Rank A) in card W & Rank A in W ) )
 for B being Ordinal holds S1[B] from ORDINAL2:sch_1(Lm2, Lm3, Lm4);
hence  ( W is Tarski & A in On W implies ( card (Rank A) in card W & Rank A in W ) ) ; ::_thesis: verum
end;

theorem :: CLASSES2:26
for A being Ordinal
for W being set st A in On (Tarski-Class W) holds
( card (Rank A) in card (Tarski-Class W) & Rank A in Tarski-Class W ) by Th25;

theorem Th27: :: CLASSES2:27
for W being set st W is Tarski holds
Rank (card W) c= W
proof
let W be set ; ::_thesis: ( W is Tarski implies Rank (card W) c= W )
assume A1: W is Tarski ; ::_thesis: Rank (card W) c= W
now__::_thesis:_(_W_<>_{}_implies_Rank_(card_W)_c=_W_)
assume A2: W <> {} ; ::_thesis: Rank (card W) c= W
thus  Rank (card W) c= W ::_thesis: verum
proof
A3: card W is limit_ordinal by A1, Th19;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Rank (card W) or x in W )
assume  x in Rank (card W) ; ::_thesis: x in W
then consider A being Ordinal such that
A4: A in card W and
A5: x in Rank A by A2, A3, CLASSES1:31;
 A in On W by A1, A4, Th9;
then  Rank A c= W by A1, Th7, Th25;
hence  x in W by A5; ::_thesis: verum
end;
end;
hence  Rank (card W) c= W by CLASSES1:29; ::_thesis: verum
end;

theorem Th28: :: CLASSES2:28
for W being set holds Rank (card (Tarski-Class W)) c= Tarski-Class W
proof
let W be set ; ::_thesis: Rank (card (Tarski-Class W)) c= Tarski-Class W
A1: card (Tarski-Class W) is limit_ordinal by Th21;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Rank (card (Tarski-Class W)) or x in Tarski-Class W )
assume  x in Rank (card (Tarski-Class W)) ; ::_thesis: x in Tarski-Class W
then consider A being Ordinal such that
A2: A in card (Tarski-Class W) and
A3: x in Rank A by A1, CLASSES1:31;
 A in On (Tarski-Class W) by A2, Th9;
then  Rank A c= Tarski-Class W by Th7, Th25;
hence  x in Tarski-Class W by A3; ::_thesis: verum
end;

deffunc H1( set ) ->  set = the_rank_of $1;

deffunc H2( set ) ->  set = card (bool $1);

theorem Th29: :: CLASSES2:29
for W, X being set st W is Tarski & W is epsilon-transitive & X in W holds
the_rank_of X in W
proof
let W, X be set ; ::_thesis: ( W is Tarski & W is epsilon-transitive & X in W implies the_rank_of X in W )
assume that
A1: W is Tarski and
A2: W is epsilon-transitive ; ::_thesis: ( not X in W or the_rank_of X in W )
A3: On W = card W by A1, Th9;
defpred S2[ Ordinal] means  ex X being set st
( $1 = the_rank_of X & X in W & not $1 in W );
assume that
A4: X in W and
A5: not the_rank_of X in W ; ::_thesis: contradiction
A6: ex A being Ordinal st S2[A] by A4, A5;
consider A being Ordinal such that
A7: S2[A] and
A8: for B being Ordinal st S2[B] holds
A c= B from ORDINAL1:sch_1(A6);
consider X being set  such that
A9: A = the_rank_of X and
A10: X in W and
A11: not A in W by A7;
defpred S3[ set ] means  ex Y being set st
( Y in X & $1 = the_rank_of Y );
consider LL being set  such that
A12: for x being set holds
( x in LL iff ( x in On W & S3[x] ) ) from XBOOLE_0:sch_1();
consider ff being Cardinal-Function such that
A13: ( dom ff = LL & ( for x being set st x in LL holds
ff . x = H2(x) ) ) from CARD_3:sch_1();
A14: LL c= On W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LL or x in On W )
thus  ( not x in LL or x in On W ) by A12; ::_thesis: verum
end;
A15: product ff c= Funcs (LL,W)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product ff or x in Funcs (LL,W) )
assume  x in product ff ; ::_thesis: x in Funcs (LL,W)
then consider g being Function such that
A16: x = g and
A17: dom g = dom ff and
A18: for x being set st x in dom ff holds
g . x in ff . x by CARD_3:def_5;
 rng g c= W
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in W )
assume  y in rng g ; ::_thesis: y in W
then consider x being set  such that
A19: x in dom g and
A20: y = g . x by FUNCT_1:def_3;
A21: ff . x = card (bool x) by A13, A17, A19;
 x in W by A14, A13, A17, A19, ORDINAL1:def_9;
then  bool x in W by A1, CLASSES1:def_2;
then  card (bool x) in W by A1, Th11;
then A22: card (bool x) c= W by A1, Th5;
 y in ff . x by A17, A18, A19, A20;
hence  y in W by A21, A22; ::_thesis: verum
end;
hence  x in Funcs (LL,W) by A13, A16, A17, FUNCT_2:def_2; ::_thesis: verum
end;
now__::_thesis:_for_Z_being_set_st_Z_in_union_LL_holds_
(_Z_is_Ordinal_&_Z_c=_union_LL_)
let Z be set ; ::_thesis: ( Z in union LL implies ( Z is Ordinal & Z c= union LL ) )
assume  Z in union LL ; ::_thesis: ( Z is Ordinal & Z c= union LL )
then consider Y being set  such that
A23: Z in Y and
A24: Y in LL by TARSKI:def_4;
 Y in On W by A12, A24;
then reconsider Y = Y as Ordinal by ORDINAL1:def_9;
A25: Y c= union LL by A24, ZFMISC_1:74;
A26: Z in Y by A23;
hence  Z is Ordinal ; ::_thesis: Z c= union LL
reconsider A = Z as Ordinal by A26;
 A c= Y by A23, ORDINAL1:def_2;
hence  Z c= union LL by A25, XBOOLE_1:1; ::_thesis: verum
end;
then reconsider ULL = union LL as Ordinal by ORDINAL1:19;
A27: dom (Card (id LL)) = dom (id LL) by CARD_3:def_2;
A28: dom (id LL) = LL by RELAT_1:45;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Card_(id_LL))_holds_
(Card_(id_LL))_._x_in_ff_._x
let x be set ; ::_thesis: ( x in dom (Card (id LL)) implies (Card (id LL)) . x in ff . x )
assume A29: x in dom (Card (id LL)) ; ::_thesis: (Card (id LL)) . x in ff . x
then A30: (Card (id LL)) . x = card ((id LL) . x) by A27, CARD_3:def_2;
A31: (id LL) . x = x by A28, A27, A29, FUNCT_1:18;
 ff . x = card (bool x) by A13, A28, A27, A29;
hence  (Card (id LL)) . x in ff . x by A31, A30, CARD_1:14; ::_thesis: verum
end;
then A32: Sum (Card (id LL)) in Product ff by A13, A28, A27, CARD_3:41;
Union (id LL) = union (rng (id LL)) by CARD_3:def_4
.= ULL by RELAT_1:45 ;
then A33: card ULL in Product ff by A32, CARD_3:39, ORDINAL1:12;
consider f being Function such that
A34: ( dom f = X & ( for x being set st x in X holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
 LL c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LL or x in rng f )
assume  x in LL ; ::_thesis: x in rng f
then consider Y being set  such that
A35: Y in X and
A36: x = the_rank_of Y by A12;
 f . Y = x by A34, A35, A36;
hence  x in rng f by A34, A35, FUNCT_1:def_3; ::_thesis: verum
end;
then A37: card LL c= card X by A34, CARD_1:12;
 card X in card W by A1, A10, Th1;
then  card LL <> card W by A37, ORDINAL1:12;
then A38: not LL,W are_equipotent by CARD_1:5;
A39: card (product ff) = Product ff by CARD_3:def_8;
A40: X c= W by A2, A10, ORDINAL1:def_2;
 X c= Rank (card W)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Rank (card W) )
assume A41: x in X ; ::_thesis: x in Rank (card W)
then  not A c= the_rank_of x by A9, CLASSES1:68, ORDINAL1:5;
then  the_rank_of x in W by A8, A40, A41;
then  the_rank_of x in card W by A3, ORDINAL1:def_9;
then A42: Rank (the_rank_of x) in Rank (card W) by CLASSES1:36;
 x c= Rank (the_rank_of x) by CLASSES1:def_8;
hence  x in Rank (card W) by A42, CLASSES1:41; ::_thesis: verum
end;
then A43: A c= On W by A9, A3, CLASSES1:65;
 On W c= ULL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in On W or x in ULL )
assume A44: x in On W ; ::_thesis: x in ULL
then reconsider B = x as Ordinal by ORDINAL1:def_9;
now__::_thesis:_ex_Y_being_set_st_
(_Y_in_X_&_not_the_rank_of_Y_c=_B_)
assume A45: for Y being set st Y in X holds
the_rank_of Y c= B ; ::_thesis: contradiction
 X c= Rank (succ B)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X or y in Rank (succ B) )
assume  y in X ; ::_thesis: y in Rank (succ B)
then  the_rank_of y c= B by A45;
then  the_rank_of y in succ B by ORDINAL1:22;
hence  y in Rank (succ B) by CLASSES1:66; ::_thesis: verum
end;
then A46: A c= succ B by A9, CLASSES1:65;
 B in W by A44, ORDINAL1:def_9;
then  succ B in W by A1, Th5;
hence  contradiction by A1, A11, A46, CLASSES1:def_1; ::_thesis: verum
end;
then consider Y being set  such that
A47: Y in X and
A48: not the_rank_of Y c= B ;
 the_rank_of Y in A by A9, A47, CLASSES1:68;
then  the_rank_of Y in LL by A43, A12, A47;
then A49: the_rank_of Y c= ULL by ZFMISC_1:74;
 B in the_rank_of Y by A48, ORDINAL1:16;
hence  x in ULL by A49; ::_thesis: verum
end;
then A50: card (On W) c= card ULL by CARD_1:11;
 On W c= W by ORDINAL2:7;
then  LL c= W by A14, XBOOLE_1:1;
then  LL in W by A1, A38, CLASSES1:def_2;
then  Funcs (LL,W) c= W by A1, A2, Th22;
then  product ff c= W by A15, XBOOLE_1:1;
then A51: Product ff c= card W by A39, CARD_1:11;
 On W = card W by A1, Th9;
hence  contradiction by A33, A51, A50, CARD_1:4; ::_thesis: verum
end;

theorem Th30: :: CLASSES2:30
for W being set st W is Tarski & W is epsilon-transitive holds
W c= Rank (card W)
proof
let W be set ; ::_thesis: ( W is Tarski & W is epsilon-transitive implies W c= Rank (card W) )
assume that
A1: W is Tarski and
A2: W is epsilon-transitive ; ::_thesis: W c= Rank (card W)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W or x in Rank (card W) )
assume  x in W ; ::_thesis: x in Rank (card W)
then  the_rank_of x in W by A1, A2, Th29;
then A3: the_rank_of x in On W by ORDINAL1:def_9;
 On W = card W by A1, Th9;
then A4: Rank (the_rank_of x) in Rank (card W) by A3, CLASSES1:36;
 x c= Rank (the_rank_of x) by CLASSES1:def_8;
hence  x in Rank (card W) by A4, CLASSES1:41; ::_thesis: verum
end;

theorem Th31: :: CLASSES2:31
for W being set st W is Tarski & W is epsilon-transitive holds
Rank (card W) = W
proof
let W be set ; ::_thesis: ( W is Tarski & W is epsilon-transitive implies Rank (card W) = W )
assume that
A1: W is Tarski and
A2: W is epsilon-transitive ; ::_thesis: Rank (card W) = W
thus  ( Rank (card W) c= W & W c= Rank (card W) ) by A1, A2, Th27, Th30; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;

theorem :: CLASSES2:32
for A being Ordinal
for W being set st W is Tarski & A in On W holds
card (Rank A) c= card W
proof
let A be Ordinal; ::_thesis: for W being set st W is Tarski & A in On W holds
card (Rank A) c= card W
let W be set ; ::_thesis: ( W is Tarski & A in On W implies card (Rank A) c= card W )
assume that
A1: W is Tarski and
A2: A in On W ; ::_thesis: card (Rank A) c= card W
 card (Rank A) in card W by A1, A2, Th25;
hence  card (Rank A) c= card W by CARD_1:3; ::_thesis: verum
end;

theorem :: CLASSES2:33
for A being Ordinal
for W being set st A in On (Tarski-Class W) holds
card (Rank A) c= card (Tarski-Class W)
proof
let A be Ordinal; ::_thesis: for W being set st A in On (Tarski-Class W) holds
card (Rank A) c= card (Tarski-Class W)
let W be set ; ::_thesis: ( A in On (Tarski-Class W) implies card (Rank A) c= card (Tarski-Class W) )
assume  A in On (Tarski-Class W) ; ::_thesis: card (Rank A) c= card (Tarski-Class W)
then  card (Rank A) in card (Tarski-Class W) by Th25;
hence  card (Rank A) c= card (Tarski-Class W) by CARD_1:3; ::_thesis: verum
end;

theorem Th34: :: CLASSES2:34
for W being set st W is Tarski holds
card W = card (Rank (card W))
proof
let W be set ; ::_thesis: ( W is Tarski implies card W = card (Rank (card W)) )
assume  W is Tarski ; ::_thesis: card W = card (Rank (card W))
then A1: card (Rank (card W)) c= card W by Th27, CARD_1:11;
 card (card W) c= card (Rank (card W)) by CARD_1:11, CLASSES1:38;
hence  card W = card (Rank (card W)) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: CLASSES2:35
for W being set holds card (Tarski-Class W) = card (Rank (card (Tarski-Class W))) by Th34;

theorem Th36: :: CLASSES2:36
for W, X being set st W is Tarski & X c= Rank (card W) & not X, Rank (card W) are_equipotent holds
X in Rank (card W)
proof
let W, X be set ; ::_thesis: ( W is Tarski & X c= Rank (card W) & not X, Rank (card W) are_equipotent implies X in Rank (card W) )
assume that
A1: W is Tarski and
A2: X c= Rank (card W) and
A3: not X, Rank (card W) are_equipotent ; ::_thesis: X in Rank (card W)
defpred S2[ set ] means  ex Y being set st
( Y in X & $1 = the_rank_of Y );
consider LL being set  such that
A4: for x being set holds
( x in LL iff ( x in On W & S2[x] ) ) from XBOOLE_0:sch_1();
consider ff being Cardinal-Function such that
A5: ( dom ff = LL & ( for x being set st x in LL holds
ff . x = H2(x) ) ) from CARD_3:sch_1();
A6: LL c= On W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LL or x in On W )
thus  ( not x in LL or x in On W ) by A4; ::_thesis: verum
end;
A7: product ff c= Funcs (LL,W)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product ff or x in Funcs (LL,W) )
assume  x in product ff ; ::_thesis: x in Funcs (LL,W)
then consider g being Function such that
A8: x = g and
A9: dom g = dom ff and
A10: for x being set st x in dom ff holds
g . x in ff . x by CARD_3:def_5;
 rng g c= W
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in W )
assume  y in rng g ; ::_thesis: y in W
then consider x being set  such that
A11: x in dom g and
A12: y = g . x by FUNCT_1:def_3;
A13: ff . x = card (bool x) by A5, A9, A11;
 x in W by A6, A5, A9, A11, ORDINAL1:def_9;
then  bool x in W by A1, CLASSES1:def_2;
then  card (bool x) in W by A1, Th11;
then A14: card (bool x) c= W by A1, Th5;
 y in ff . x by A9, A10, A11, A12;
hence  y in W by A13, A14; ::_thesis: verum
end;
hence  x in Funcs (LL,W) by A5, A8, A9, FUNCT_2:def_2; ::_thesis: verum
end;
A15: card W = card (Rank (card W)) by A1, Th34;
then A16: card X <> card W by A3, CARD_1:5;
 On W c= W by ORDINAL2:7;
then A17: LL c= W by A6, XBOOLE_1:1;
now__::_thesis:_for_Z_being_set_st_Z_in_union_LL_holds_
(_Z_is_Ordinal_&_Z_c=_union_LL_)
let Z be set ; ::_thesis: ( Z in union LL implies ( Z is Ordinal & Z c= union LL ) )
assume  Z in union LL ; ::_thesis: ( Z is Ordinal & Z c= union LL )
then consider Y being set  such that
A18: Z in Y and
A19: Y in LL by TARSKI:def_4;
 Y in On W by A4, A19;
then reconsider Y = Y as Ordinal by ORDINAL1:def_9;
A20: Y c= union LL by A19, ZFMISC_1:74;
A21: Z in Y by A18;
hence  Z is Ordinal ; ::_thesis: Z c= union LL
reconsider A = Z as Ordinal by A21;
 A c= Y by A18, ORDINAL1:def_2;
hence  Z c= union LL by A20, XBOOLE_1:1; ::_thesis: verum
end;
then reconsider ULL = union LL as Ordinal by ORDINAL1:19;
A22: dom (Card (id LL)) = dom (id LL) by CARD_3:def_2;
A23: dom (id LL) = LL by RELAT_1:45;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Card_(id_LL))_holds_
(Card_(id_LL))_._x_in_ff_._x
let x be set ; ::_thesis: ( x in dom (Card (id LL)) implies (Card (id LL)) . x in ff . x )
assume A24: x in dom (Card (id LL)) ; ::_thesis: (Card (id LL)) . x in ff . x
then A25: (Card (id LL)) . x = card ((id LL) . x) by A22, CARD_3:def_2;
A26: (id LL) . x = x by A23, A22, A24, FUNCT_1:18;
 ff . x = card (bool x) by A5, A23, A22, A24;
hence  (Card (id LL)) . x in ff . x by A26, A25, CARD_1:14; ::_thesis: verum
end;
then A27: Sum (Card (id LL)) in Product ff by A5, A23, A22, CARD_3:41;
consider f being Function such that
A28: ( dom f = X & ( for x being set st x in X holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
 LL c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LL or x in rng f )
assume  x in LL ; ::_thesis: x in rng f
then consider Y being set  such that
A29: Y in X and
A30: x = the_rank_of Y by A4;
 f . Y = x by A28, A29, A30;
hence  x in rng f by A28, A29, FUNCT_1:def_3; ::_thesis: verum
end;
then A31: card LL c= card X by A28, CARD_1:12;
A32: card (product ff) = Product ff by CARD_3:def_8;
 card X c= card W by A2, A15, CARD_1:11;
then  card X in card W by A16, CARD_1:3;
then  card LL <> card W by A31, ORDINAL1:12;
then  not LL,W are_equipotent by CARD_1:5;
then  LL in W by A1, A17, CLASSES1:def_2;
then  Funcs (LL,W) c= W by A1, A17, Th22;
then  product ff c= W by A7, XBOOLE_1:1;
then A33: Product ff c= card W by A32, CARD_1:11;
A34: card W is limit_ordinal by A1, Th19;
A35: card W = On W by A1, Th9;
 X c= Rank (succ ULL)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Rank (succ ULL) )
defpred S3[ Ordinal] means ( $1 in card W & x c= Rank $1 );
assume A36: x in X ; ::_thesis: x in Rank (succ ULL)
then A37: f . x = the_rank_of x by A28;
consider A being Ordinal such that
A38: A in card W and
A39: x in Rank A by A2, A34, A36, CLASSES1:29, CLASSES1:31;
 S3[A] by A38, A39, ORDINAL1:def_2;
then A40: ex A being Ordinal st S3[A] ;
consider A being Ordinal such that
A41: S3[A] and
A42: for B being Ordinal st S3[B] holds
A c= B from ORDINAL1:sch_1(A40);
now__::_thesis:_for_B_being_Ordinal_st_x_c=_Rank_B_holds_
A_c=_B
let B be Ordinal; ::_thesis: ( x c= Rank B implies A c= B )
assume  x c= Rank B ; ::_thesis: A c= B
then  ( ( A c= card W & card W c= B ) or A c= B ) by A41, A42, ORDINAL1:16;
hence  A c= B by XBOOLE_1:1; ::_thesis: verum
end;
then  A = the_rank_of x by A41, CLASSES1:def_8;
then  f . x in LL by A4, A35, A36, A37, A41;
then  the_rank_of x c= ULL by A37, ZFMISC_1:74;
then A43: Rank (the_rank_of x) c= Rank ULL by CLASSES1:37;
 x c= Rank (the_rank_of x) by CLASSES1:def_8;
then  x c= Rank ULL by A43, XBOOLE_1:1;
hence  x in Rank (succ ULL) by CLASSES1:32; ::_thesis: verum
end;
then A44: X in Rank (succ (succ ULL)) by CLASSES1:32;
Union (id LL) = union (rng (id LL)) by CARD_3:def_4
.= ULL by RELAT_1:45 ;
then  card ULL in card W by A27, A33, CARD_3:39, ORDINAL1:12;
then A45: ULL <> On W by A35;
 union (card W) = card W by A34, ORDINAL1:def_6;
then  ULL c= On W by A6, A35, ZFMISC_1:77;
then  ULL c< On W by A45, XBOOLE_0:def_8;
then  ULL in card W by A35, ORDINAL1:11;
then  succ ULL in card W by A34, ORDINAL1:28;
then  succ (succ ULL) in card W by A34, ORDINAL1:28;
hence  X in Rank (card W) by A34, A44, CLASSES1:31; ::_thesis: verum
end;

theorem :: CLASSES2:37
for X, W being set holds
( not X c= Rank (card (Tarski-Class W)) or X, Rank (card (Tarski-Class W)) are_equipotent or X in Rank (card (Tarski-Class W)) ) by Th36;

theorem Th38: :: CLASSES2:38
for W being set st W is Tarski holds
Rank (card W) is Tarski
proof
let W be set ; ::_thesis: ( W is Tarski implies Rank (card W) is Tarski )
assume A1: W is Tarski ; ::_thesis: Rank (card W) is Tarski
set B = Rank (card W);
thus  for X, Y being set st X in Rank (card W) & Y c= X holds
Y in Rank (card W) by CLASSES1:41; :: according to CLASSES1:def_1,CLASSES1:def_2 ::_thesis: ( ( for b1 being set holds
( not b1 in Rank (card W) or bool b1 in Rank (card W) ) ) & ( for b1 being set holds
( not b1 c= Rank (card W) or b1, Rank (card W) are_equipotent or b1 in Rank (card W) ) ) )
now__::_thesis:_(_W_<>_{}_implies_for_X_being_set_st_X_in_Rank_(card_W)_holds_
bool_X_in_Rank_(card_W)_)
A2: card W is limit_ordinal by A1, Th19;
assume A3: W <> {} ; ::_thesis: for X being set st X in Rank (card W) holds
bool X in Rank (card W)
thus  for X being set st X in Rank (card W) holds
bool X in Rank (card W) ::_thesis: verum
proof
let X be set ; ::_thesis: ( X in Rank (card W) implies bool X in Rank (card W) )
assume  X in Rank (card W) ; ::_thesis: bool X in Rank (card W)
then consider A being Ordinal such that
A4: A in card W and
A5: X in Rank A by A3, A2, CLASSES1:31;
A6: bool X in Rank (succ A) by A5, CLASSES1:42;
 succ A in card W by A2, A4, ORDINAL1:28;
hence  bool X in Rank (card W) by A2, A6, CLASSES1:31; ::_thesis: verum
end;
end;
hence  ( ( for b1 being set holds
( not b1 in Rank (card W) or bool b1 in Rank (card W) ) ) & ( for b1 being set holds
( not b1 c= Rank (card W) or b1, Rank (card W) are_equipotent or b1 in Rank (card W) ) ) ) by A1, Th36, CLASSES1:29; ::_thesis: verum
end;

theorem :: CLASSES2:39
for W being set holds Rank (card (Tarski-Class W)) is Tarski by Th38;

theorem Th40: :: CLASSES2:40
for A being Ordinal
for X being set st X is epsilon-transitive & A in the_rank_of X holds
ex Y being set st
( Y in X & the_rank_of Y = A )
proof
let A be Ordinal; ::_thesis: for X being set st X is epsilon-transitive & A in the_rank_of X holds
ex Y being set st
( Y in X & the_rank_of Y = A )
let X be set ; ::_thesis: ( X is epsilon-transitive & A in the_rank_of X implies ex Y being set st
( Y in X & the_rank_of Y = A ) )
assume that
A1: X is epsilon-transitive and
A2: A in the_rank_of X ; ::_thesis: ex Y being set st
( Y in X & the_rank_of Y = A )
defpred S2[ Ordinal] means  ex Y being set st
( A in $1 & Y in X & the_rank_of Y = $1 );
assume A3: for Y being set holds
( not Y in X or not the_rank_of Y = A ) ; ::_thesis: contradiction
A4: ex B being Ordinal st S2[B]
proof
assume A5: for B being Ordinal
for Y being set st A in B & Y in X holds
the_rank_of Y <> B ; ::_thesis: contradiction
 X c= Rank A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Rank A )
assume A6: x in X ; ::_thesis: x in Rank A
then A7: the_rank_of x <> A by A3;
 the_rank_of x c= A by A5, A6, ORDINAL1:16;
then  the_rank_of x c< A by A7, XBOOLE_0:def_8;
then  the_rank_of x in A by ORDINAL1:11;
hence  x in Rank A by CLASSES1:66; ::_thesis: verum
end;
then  the_rank_of X c= A by CLASSES1:65;
hence  contradiction by A2, ORDINAL1:5; ::_thesis: verum
end;
consider B being Ordinal such that
A8: S2[B] and
A9: for C being Ordinal st S2[C] holds
B c= C from ORDINAL1:sch_1(A4);
consider Y being set  such that
A10: A in B and
A11: Y in X and
A12: the_rank_of Y = B by A8;
 Y c= Rank A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in Rank A )
A13: Y c= X by A1, A11, ORDINAL1:def_2;
assume A14: x in Y ; ::_thesis: x in Rank A
then  the_rank_of x in B by A12, CLASSES1:68;
then  not A in the_rank_of x by A9, A14, A13, ORDINAL1:5;
then A15: the_rank_of x c= A by ORDINAL1:16;
 the_rank_of x <> A by A3, A14, A13;
then  the_rank_of x c< A by A15, XBOOLE_0:def_8;
then  the_rank_of x in A by ORDINAL1:11;
hence  x in Rank A by CLASSES1:66; ::_thesis: verum
end;
then  the_rank_of Y c= A by CLASSES1:65;
hence  contradiction by A10, A12, ORDINAL1:5; ::_thesis: verum
end;

theorem Th41: :: CLASSES2:41
for X being set st X is epsilon-transitive holds
card (the_rank_of X) c= card X
proof
let X be set ; ::_thesis: ( X is epsilon-transitive implies card (the_rank_of X) c= card X )
consider f being Function such that
A1: ( dom f = X & ( for x being set st x in X holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
assume A2: X is epsilon-transitive ; ::_thesis: card (the_rank_of X) c= card X
 the_rank_of X c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the_rank_of X or x in rng f )
assume A3: x in the_rank_of X ; ::_thesis: x in rng f
then reconsider x9 = x as Ordinal ;
consider Y being set  such that
A4: Y in X and
A5: the_rank_of Y = x9 by A2, A3, Th40;
 f . Y = x by A1, A4, A5;
hence  x in rng f by A1, A4, FUNCT_1:def_3; ::_thesis: verum
end;
hence  card (the_rank_of X) c= card X by A1, CARD_1:12; ::_thesis: verum
end;

theorem Th42: :: CLASSES2:42
for W, X being set st W is Tarski & X is epsilon-transitive & X in W holds
X in Rank (card W)
proof
let W, X be set ; ::_thesis: ( W is Tarski & X is epsilon-transitive & X in W implies X in Rank (card W) )
assume A1: W is Tarski ; ::_thesis: ( not X is epsilon-transitive or not X in W or X in Rank (card W) )
assume A2: X is epsilon-transitive ; ::_thesis: ( not X in W or X in Rank (card W) )
assume  X in W ; ::_thesis: X in Rank (card W)
then  card X in card W by A1, Th1;
then A3: card (the_rank_of X) in card W by A2, Th41, ORDINAL1:12;
 card (card W) = card W ;
then  the_rank_of X in card W by A3, CARD_3:43;
then A4: Rank (the_rank_of X) in Rank (card W) by CLASSES1:36;
 X c= Rank (the_rank_of X) by CLASSES1:def_8;
hence  X in Rank (card W) by A4, CLASSES1:41; ::_thesis: verum
end;

theorem :: CLASSES2:43
for X, W being set st X is epsilon-transitive & X in Tarski-Class W holds
X in Rank (card (Tarski-Class W)) by Th42;

theorem Th44: :: CLASSES2:44
for W being set st W is epsilon-transitive holds
Rank (card (Tarski-Class W)) is_Tarski-Class_of W
proof
let W be set ; ::_thesis: ( W is epsilon-transitive implies Rank (card (Tarski-Class W)) is_Tarski-Class_of W )
A1: W in Tarski-Class W by CLASSES1:2;
assume  W is epsilon-transitive ; ::_thesis: Rank (card (Tarski-Class W)) is_Tarski-Class_of W
hence  ( W in Rank (card (Tarski-Class W)) & Rank (card (Tarski-Class W)) is Tarski ) by A1, Th38, Th42; :: according to CLASSES1:def_3 ::_thesis: verum
end;

theorem :: CLASSES2:45
for W being set st W is epsilon-transitive holds
Rank (card (Tarski-Class W)) = Tarski-Class W
proof
let W be set ; ::_thesis: ( W is epsilon-transitive implies Rank (card (Tarski-Class W)) = Tarski-Class W )
assume  W is epsilon-transitive ; ::_thesis: Rank (card (Tarski-Class W)) = Tarski-Class W
then  Rank (card (Tarski-Class W)) is_Tarski-Class_of W by Th44;
hence  ( Rank (card (Tarski-Class W)) c= Tarski-Class W & Tarski-Class W c= Rank (card (Tarski-Class W)) ) by Th28, CLASSES1:def_4; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;

definition
let IT be set ;
attrIT is universal  means :Def1: :: CLASSES2:def 1
( IT is epsilon-transitive & IT is Tarski );
end;

:: deftheorem Def1 defines universal CLASSES2:def_1_:_
 for IT being set holds
( IT is universal iff ( IT is epsilon-transitive & IT is Tarski ) );

registration
cluster universal  ->  epsilon-transitive Tarski for set ;
coherence
 for b1 being set st b1 is universal holds
( b1 is epsilon-transitive & b1 is Tarski ) by Def1;
cluster epsilon-transitive Tarski  ->  universal for set ;
coherence
 for b1 being set st b1 is epsilon-transitive & b1 is Tarski holds
b1 is universal by Def1;
end;

registration
cluster non empty universal for set ;
existence
 ex b1 being set st
( b1 is universal & not b1 is empty )
proof
set X = the set ;
take V = Tarski-Class (the_transitive-closure_of the set ); ::_thesis: ( V is universal & not V is empty )
thus  V is epsilon-transitive by CLASSES1:23, CLASSES1:51; :: according to CLASSES2:def_1 ::_thesis: ( V is Tarski & not V is empty )
thus  ( V is Tarski & not V is empty ) ; ::_thesis: verum
end;
end;

definition
mode Universe is non empty universal set ;
end;


theorem Th46: :: CLASSES2:46
for U being Universe holds On U is Ordinal
proof
let U be Universe; ::_thesis: On U is Ordinal
 On U = card U by Th9;
hence  On U is Ordinal ; ::_thesis: verum
end;

theorem Th47: :: CLASSES2:47
for X being set st X is epsilon-transitive holds
Tarski-Class X is universal
proof
let X be set ; ::_thesis: ( X is epsilon-transitive implies Tarski-Class X is universal )
assume  X is epsilon-transitive ; ::_thesis: Tarski-Class X is universal
hence  ( Tarski-Class X is epsilon-transitive & Tarski-Class X is Tarski ) by CLASSES1:23; :: according to CLASSES2:def_1 ::_thesis: verum
end;

theorem :: CLASSES2:48
for U being Universe holds Tarski-Class U is Universe by Th47;

registration
let U be Universe;
cluster On U ->  ordinal ;
coherence
 On U is ordinal by Th46;
cluster Tarski-Class U ->  universal ;
coherence
 Tarski-Class U is universal by Th47;
end;

theorem Th49: :: CLASSES2:49
for A being Ordinal holds Tarski-Class A is universal
proof
let A be Ordinal; ::_thesis: Tarski-Class A is universal
set M = Tarski-Class A;
thus  ( Tarski-Class A is epsilon-transitive & Tarski-Class A is Tarski ) by CLASSES1:23; :: according to CLASSES2:def_1 ::_thesis: verum
end;

registration
let A be Ordinal;
cluster Tarski-Class A ->  universal ;
coherence
 Tarski-Class A is universal by Th49;
end;

theorem Th50: :: CLASSES2:50
for U being Universe holds U = Rank (On U)
proof
let U be Universe; ::_thesis: U = Rank (On U)
 card U = On U by Th9;
hence  U = Rank (On U) by Th31; ::_thesis: verum
end;

theorem Th51: :: CLASSES2:51
for U being Universe holds
( On U <> {} & On U is limit_ordinal )
proof
let U be Universe; ::_thesis: ( On U <> {} & On U is limit_ordinal )
 card U = On U by Th9;
hence  ( On U <> {} & On U is limit_ordinal ) by Th19; ::_thesis: verum
end;

theorem :: CLASSES2:52
for U1, U2 being Universe holds
( U1 in U2 or U1 = U2 or U2 in U1 )
proof
let U1, U2 be Universe; ::_thesis: ( U1 in U2 or U1 = U2 or U2 in U1 )
A1: ( On U1 in On U2 or On U1 = On U2 or On U2 in On U1 ) by ORDINAL1:14;
A2: U2 = Rank (On U2) by Th50;
 U1 = Rank (On U1) by Th50;
hence  ( U1 in U2 or U1 = U2 or U2 in U1 ) by A1, A2, CLASSES1:36; ::_thesis: verum
end;

theorem Th53: :: CLASSES2:53
for U1, U2 being Universe holds
( U1 c= U2 or U2 in U1 )
proof
let U1, U2 be Universe; ::_thesis: ( U1 c= U2 or U2 in U1 )
A1: ( On U1 c= On U2 or On U2 in On U1 ) by ORDINAL1:16;
A2: U2 = Rank (On U2) by Th50;
 U1 = Rank (On U1) by Th50;
hence  ( U1 c= U2 or U2 in U1 ) by A1, A2, CLASSES1:36, CLASSES1:37; ::_thesis: verum
end;

theorem Th54: :: CLASSES2:54
for U1, U2 being Universe holds U1,U2 are_c=-comparable
proof
let U1, U2 be Universe; ::_thesis: U1,U2 are_c=-comparable
A1: ( On U1 c= On U2 or On U2 c= On U1 ) ;
A2: U2 = Rank (On U2) by Th50;
 U1 = Rank (On U1) by Th50;
hence  ( U1 c= U2 or U2 c= U1 ) by A1, A2, CLASSES1:37; :: according to XBOOLE_0:def_9 ::_thesis: verum
end;

theorem :: CLASSES2:55
for U1, U2 being Universe holds
( U1 \/ U2 is Universe & U1 /\ U2 is Universe )
proof
let U1, U2 be Universe; ::_thesis: ( U1 \/ U2 is Universe & U1 /\ U2 is Universe )
 U1,U2 are_c=-comparable by Th54;
then  ( U1 c= U2 or U2 c= U1 ) by XBOOLE_0:def_9;
hence  ( U1 \/ U2 is Universe & U1 /\ U2 is Universe ) by XBOOLE_1:12, XBOOLE_1:28; ::_thesis: verum
end;

theorem Th56: :: CLASSES2:56
for U being Universe holds {} in U
proof
let U be Universe; ::_thesis: {} in U
 {} c= the Element of U by XBOOLE_1:2;
hence  {} in U by CLASSES1:def_1; ::_thesis: verum
end;

theorem :: CLASSES2:57
for x being set
for U being Universe st x in U holds
{x} in U by Th2;

theorem :: CLASSES2:58
for x, y being set
for U being Universe st x in U & y in U holds
( {x,y} in U & [x,y] in U ) by Th2, Th3;

theorem Th59: :: CLASSES2:59
for X being set
for U being Universe st X in U holds
( bool X in U & union X in U & meet X in U )
proof
let X be set ; ::_thesis: for U being Universe st X in U holds
( bool X in U & union X in U & meet X in U )
let U be Universe; ::_thesis: ( X in U implies ( bool X in U & union X in U & meet X in U ) )
assume A1: X in U ; ::_thesis: ( bool X in U & union X in U & meet X in U )
hence  bool X in U by CLASSES1:def_2; ::_thesis: ( union X in U & meet X in U )
 U = Rank (On U) by Th50;
hence A2: union X in U by A1, CLASSES1:35; ::_thesis: meet X in U
 meet X c= union X by SETFAM_1:2;
hence  meet X in U by A2, CLASSES1:def_1; ::_thesis: verum
end;

theorem Th60: :: CLASSES2:60
for X, Y being set
for U being Universe st X in U & Y in U holds
( X \/ Y in U & X /\ Y in U & X \ Y in U & X \+\ Y in U )
proof
let X, Y be set ; ::_thesis: for U being Universe st X in U & Y in U holds
( X \/ Y in U & X /\ Y in U & X \ Y in U & X \+\ Y in U )
let U be Universe; ::_thesis: ( X in U & Y in U implies ( X \/ Y in U & X /\ Y in U & X \ Y in U & X \+\ Y in U ) )
assume that
A1: X in U and
A2: Y in U ; ::_thesis: ( X \/ Y in U & X /\ Y in U & X \ Y in U & X \+\ Y in U )
A3: union {X,Y} = X \/ Y by ZFMISC_1:75;
A4: meet {X,Y} = X /\ Y by SETFAM_1:11;
 {X,Y} in U by A1, A2, Th2;
hence A5: ( X \/ Y in U & X /\ Y in U ) by A3, A4, Th59; ::_thesis: ( X \ Y in U & X \+\ Y in U )
 X \+\ Y = (X \/ Y) \ (X /\ Y) by XBOOLE_1:101;
hence  ( X \ Y in U & X \+\ Y in U ) by A1, A5, CLASSES1:def_1; ::_thesis: verum
end;

theorem Th61: :: CLASSES2:61
for X, Y being set
for U being Universe st X in U & Y in U holds
( [:X,Y:] in U & Funcs (X,Y) in U )
proof
let X, Y be set ; ::_thesis: for U being Universe st X in U & Y in U holds
( [:X,Y:] in U & Funcs (X,Y) in U )
let U be Universe; ::_thesis: ( X in U & Y in U implies ( [:X,Y:] in U & Funcs (X,Y) in U ) )
assume that
A1: X in U and
A2: Y in U ; ::_thesis: ( [:X,Y:] in U & Funcs (X,Y) in U )
 X \/ Y in U by A1, A2, Th60;
then  bool (X \/ Y) in U by Th59;
then A3: bool (bool (X \/ Y)) in U by Th59;
 [:X,Y:] c= bool (bool (X \/ Y)) by ZFMISC_1:86;
hence  [:X,Y:] in U by A3, CLASSES1:def_1; ::_thesis: Funcs (X,Y) in U
then A4: bool [:X,Y:] in U by Th59;
 Funcs (X,Y) c= bool [:X,Y:] by FRAENKEL:2;
hence  Funcs (X,Y) in U by A4, CLASSES1:def_1; ::_thesis: verum
end;


registration
let U1 be Universe;
cluster non empty for Element of U1;
existence
 not for b1 being Element of U1 holds b1 is empty
proof
 {} in U1 by Th56;
then reconsider x = bool {} as Element of U1 by Th59;
take  x ; ::_thesis: not x is empty
thus  not x is empty ; ::_thesis: verum
end;
end;

definition
let U be Universe;
let u be Element of U;
:: original: {
redefine func{u} ->  Element of U;
coherence
 {u} is Element of U by Th2;
:: original: bool
redefine func bool u ->  Element of U;
coherence
 bool u is Element of U by Th59;
:: original: union
redefine func union u ->  Element of U;
coherence
 union u is Element of U by Th59;
:: original: meet
redefine func meet u ->  Element of U;
coherence
 meet u is Element of U by Th59;
let v be Element of U;
:: original: {
redefine func{u,v} ->  Element of U;
coherence
 {u,v} is Element of U by Th2;
:: original: [
redefine func[u,v] ->  Element of U;
coherence
 [u,v] is Element of U by Th3;
:: original: \/
redefine funcu \/ v ->  Element of U;
coherence
 u \/ v is Element of U by Th60;
:: original: /\
redefine funcu /\ v ->  Element of U;
coherence
 u /\ v is Element of U by Th60;
:: original: \
redefine funcu \ v ->  Element of U;
coherence
 u \ v is Element of U by Th60;
:: original: \+\
redefine funcu \+\ v ->  Element of U;
coherence
 u \+\ v is Element of U by Th60;
:: original: [:
redefine func[:u,v:] ->  Element of U;
coherence
 [:u,v:] is Element of U by Th61;
:: original: Funcs
redefine func Funcs (u,v) ->  Element of U;
coherence
 Funcs (u,v) is Element of U by Th61;
end;

definition
func FinSETS  ->  Universe equals :: CLASSES2:def 2
 Tarski-Class {};
correctness
coherence
Tarski-Class {} is Universe;
;
end;

:: deftheorem  defines FinSETS CLASSES2:def_2_:_
 FinSETS = Tarski-Class {};

Lm5:  omega is limit_ordinal
by ORDINAL1:def_11;

theorem Th62: :: CLASSES2:62
card (Rank omega) = card omega
proof
deffunc H3( Ordinal) ->  set = Rank $1;
consider L being T-Sequence such that
A1: ( dom L = omega & ( for A being Ordinal st A in omega holds
L . A = H3(A) ) ) from ORDINAL2:sch_2();
now__::_thesis:_for_X,_Y_being_set_st_X_in_rng_L_&_Y_in_rng_L_holds_
X,Y_are_c=-comparable
let X, Y be set ; ::_thesis: ( X in rng L & Y in rng L implies X,Y are_c=-comparable )
assume  X in rng L ; ::_thesis: ( Y in rng L implies X,Y are_c=-comparable )
then consider x being set  such that
A2: x in dom L and
A3: X = L . x by FUNCT_1:def_3;
assume  Y in rng L ; ::_thesis: X,Y are_c=-comparable
then consider y being set  such that
A4: y in dom L and
A5: Y = L . y by FUNCT_1:def_3;
reconsider x = x, y = y as Ordinal by A2, A4;
A6: Y = Rank y by A1, A4, A5;
A7: ( x c= y or y c= x ) ;
 X = Rank x by A1, A2, A3;
then  ( X c= Y or Y c= X ) by A6, A7, CLASSES1:37;
hence  X,Y are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum
end;
then A8: rng L is c=-linear by ORDINAL1:def_8;
A9: card omega c= card (Rank omega) by CARD_1:11, CLASSES1:38;
A10: now__::_thesis:_for_X_being_set_st_X_in_rng_L_holds_
card_X_in_card_omega
let X be set ; ::_thesis: ( X in rng L implies card X in card omega )
assume  X in rng L ; ::_thesis: card X in card omega
then consider x being set  such that
A11: x in dom L and
A12: X = L . x by FUNCT_1:def_3;
reconsider x = x as Ordinal by A11;
 X = Rank x by A1, A11, A12;
hence  card X in card omega by A1, A11, CARD_2:67, CARD_3:42; ::_thesis: verum
end;
Rank omega = Union L by A1, Lm5, Th24
.= union (rng L) by CARD_3:def_4 ;
then  card (Rank omega) c= card omega by A8, A10, CARD_3:46;
hence  card (Rank omega) = card omega by A9, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th63: :: CLASSES2:63
Rank omega is Tarski
proof
thus  for X, Y being set st X in Rank omega & Y c= X holds
Y in Rank omega by CLASSES1:41; :: according to CLASSES1:def_1,CLASSES1:def_2 ::_thesis: ( ( for b1 being set holds
( not b1 in Rank omega or bool b1 in Rank omega ) ) & ( for b1 being set holds
( not b1 c= Rank omega or b1, Rank omega are_equipotent or b1 in Rank omega ) ) )
thus  for X being set st X in Rank omega holds
bool X in Rank omega ::_thesis: for b1 being set holds
( not b1 c= Rank omega or b1, Rank omega are_equipotent or b1 in Rank omega )
proof
let X be set ; ::_thesis: ( X in Rank omega implies bool X in Rank omega )
assume  X in Rank omega ; ::_thesis: bool X in Rank omega
then consider A being Ordinal such that
A1: A in omega and
A2: X in Rank A by Lm5, CLASSES1:31;
A3: bool X in Rank (succ A) by A2, CLASSES1:42;
 succ A in omega by A1, Lm5, ORDINAL1:28;
hence  bool X in Rank omega by A3, Lm5, CLASSES1:31; ::_thesis: verum
end;
thus  for X being set holds
( not X c= Rank omega or X, Rank omega are_equipotent or X in Rank omega ) ::_thesis: verum
proof
let X be set ; ::_thesis: ( not X c= Rank omega or X, Rank omega are_equipotent or X in Rank omega )
A4: 0 in omega ;
defpred S2[ set , set ] means  the_rank_of $2 c= the_rank_of $1;
assume that
A5: X c= Rank omega and
A6: not X, Rank omega are_equipotent and
A7: not X in Rank omega ; ::_thesis: contradiction
A8: card X <> card omega by A6, Th62, CARD_1:5;
 card X c= card omega by A5, Th62, CARD_1:11;
then  card X in omega by A8, CARD_1:3, CARD_1:47;
then reconsider X = X as finite set ;
A9: for x, y being set holds
( S2[x,y] or S2[y,x] ) ;
A10: for x, y, z being set st S2[x,y] & S2[y,z] holds
S2[x,z] by XBOOLE_1:1;
 omega c= Rank omega by CLASSES1:38;
then A11: X <> {} by A7, A4;
consider x being set  such that
A12: ( x in X & ( for y being set st y in X holds
S2[x,y] ) ) from CARD_2:sch_2(A11, A9, A10);
set A = the_rank_of x;
now__::_thesis:_for_Y_being_set_st_Y_in_X_holds_
the_rank_of_Y_in_succ_(the_rank_of_x)
let Y be set ; ::_thesis: ( Y in X implies the_rank_of Y in succ (the_rank_of x) )
assume  Y in X ; ::_thesis: the_rank_of Y in succ (the_rank_of x)
then  the_rank_of Y c= the_rank_of x by A12;
hence  the_rank_of Y in succ (the_rank_of x) by ORDINAL1:22; ::_thesis: verum
end;
then A13: the_rank_of X c= succ (the_rank_of x) by CLASSES1:69;
 the_rank_of x in omega by A5, A12, CLASSES1:66;
then  succ (the_rank_of x) in omega by Lm5, ORDINAL1:28;
then  the_rank_of X in omega by A13, ORDINAL1:12;
hence  contradiction by A7, CLASSES1:66; ::_thesis: verum
end;
end;

theorem :: CLASSES2:64
FinSETS = Rank omega
proof
A1: omega c= Rank omega by CLASSES1:38;
then reconsider M = Rank omega as non empty set ;
 0 in omega ;
then  M is_Tarski-Class_of {} by A1, Th63, CLASSES1:def_3;
hence  FinSETS c= Rank omega by CLASSES1:def_4; :: according to XBOOLE_0:def_10 ::_thesis: Rank omega c= FinSETS
A2: {} in On FinSETS by Th51, ORDINAL3:8;
A3: FinSETS = Rank (On FinSETS) by Th50;
 On FinSETS is limit_ordinal by Th51;
then  omega c= On FinSETS by A2, ORDINAL1:def_11;
hence  Rank omega c= FinSETS by A3, CLASSES1:37; ::_thesis: verum
end;

definition
func SETS  ->  Universe equals :: CLASSES2:def 3
 Tarski-Class FinSETS;
correctness
coherence
Tarski-Class FinSETS is Universe;
;
end;

:: deftheorem  defines SETS CLASSES2:def_3_:_
 SETS = Tarski-Class FinSETS;

registration
let X be set ;
cluster the_transitive-closure_of X ->  epsilon-transitive ;
coherence
 the_transitive-closure_of X is epsilon-transitive by CLASSES1:51;
end;

registration
let X be epsilon-transitive set ;
cluster Tarski-Class X ->  epsilon-transitive ;
coherence
 Tarski-Class X is epsilon-transitive by CLASSES1:23;
end;

definition
let X be set ;
func Universe_closure X ->  Universe means :Def4: :: CLASSES2:def 4
( X c= it & ( for Y being Universe st X c= Y holds
it c= Y ) );
uniqueness
 for b1, b2 being Universe st X c= b1 & ( for Y being Universe st X c= Y holds
b1 c= Y ) & X c= b2 & ( for Y being Universe st X c= Y holds
b2 c= Y ) holds
b1 = b2
proof
let T1, T2 be Universe; ::_thesis: ( X c= T1 & ( for Y being Universe st X c= Y holds
T1 c= Y ) & X c= T2 & ( for Y being Universe st X c= Y holds
T2 c= Y ) implies T1 = T2 )
assume A1: ( X c= T1 & ( for Y being Universe st X c= Y holds
T1 c= Y ) & X c= T2 & ( for Y being Universe st X c= Y holds
T2 c= Y ) & not T1 = T2 ) ; ::_thesis: contradiction
then A2: T2 c= T1 ;
 T1 c= T2 by A1;
hence  contradiction by A1, A2, XBOOLE_0:def_10; ::_thesis: verum
end;
existence
 ex b1 being Universe st
( X c= b1 & ( for Y being Universe st X c= Y holds
b1 c= Y ) )
proof
percases ( Rank (the_rank_of X) is Universe or not Rank (the_rank_of X) is Universe ) ;
suppose Rank (the_rank_of X) is Universe ; ::_thesis: ex b1 being Universe st
( X c= b1 & ( for Y being Universe st X c= Y holds
b1 c= Y ) )
then reconsider R = Rank (the_rank_of X) as Universe ;
take  R ; ::_thesis: ( X c= R & ( for Y being Universe st X c= Y holds
R c= Y ) )
thus  X c= R by CLASSES1:def_8; ::_thesis: for Y being Universe st X c= Y holds
R c= Y
let Y be Universe; ::_thesis: ( X c= Y implies R c= Y )
assume  X c= Y ; ::_thesis: R c= Y
then  the_rank_of X c= the_rank_of Y by CLASSES1:67;
then A3: R c= Rank (the_rank_of Y) by CLASSES1:37;
A4: Rank (card Y) = Y by Th31;
then  the_rank_of Y c= card Y by CLASSES1:def_8;
then  Rank (the_rank_of Y) c= Y by A4, CLASSES1:37;
hence  R c= Y by A3, XBOOLE_1:1; ::_thesis: verum
end;
supposeA5: Rank (the_rank_of X) is not Universe ; ::_thesis: ex b1 being Universe st
( X c= b1 & ( for Y being Universe st X c= Y holds
b1 c= Y ) )
take R = Tarski-Class (Rank (the_rank_of X)); ::_thesis: ( X c= R & ( for Y being Universe st X c= Y holds
R c= Y ) )
A6: Rank (the_rank_of X) in R by CLASSES1:2;
 X c= Rank (the_rank_of X) by CLASSES1:def_8;
then  X in R by A6, CLASSES1:def_1;
hence  X c= R by ORDINAL1:def_2; ::_thesis: for Y being Universe st X c= Y holds
R c= Y
let Y be Universe; ::_thesis: ( X c= Y implies R c= Y )
assume  X c= Y ; ::_thesis: R c= Y
then A7: the_rank_of X c= the_rank_of Y by CLASSES1:67;
A8: Rank (card Y) = Y by Th31;
then A9: the_rank_of Y c= card Y by CLASSES1:def_8;
 Y c= Rank (the_rank_of Y) by CLASSES1:def_8;
then  card Y c= the_rank_of Y by A8, CLASSES1:37;
then  card Y = the_rank_of Y by A9, XBOOLE_0:def_10;
then  the_rank_of X c< card Y by A5, A7, A8, XBOOLE_0:def_8;
then  the_rank_of X in card Y by ORDINAL1:11;
then  Rank (the_rank_of X) in Y by A8, CLASSES1:36;
then  Y is_Tarski-Class_of Rank (the_rank_of X) by CLASSES1:def_3;
hence  R c= Y by CLASSES1:def_4; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem Def4 defines Universe_closure CLASSES2:def_4_:_
 for X being set
for b2 being Universe holds
( b2 = Universe_closure X iff ( X c= b2 & ( for Y being Universe st X c= Y holds
b2 c= Y ) ) );

deffunc H3( Ordinal, set ) ->  set = Tarski-Class $2;

deffunc H4( Ordinal, T-Sequence) ->  Universe = Universe_closure (Union $2);

definition
mode FinSet is Element of FinSETS ;
mode Set is Element of SETS ;
let A be Ordinal;
func UNIVERSE A ->  set  means :Def5: :: CLASSES2:def 5
 ex L being T-Sequence st
( it = last L & dom L = succ A & L . {} = FinSETS & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = Tarski-Class (L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = Universe_closure (Union (L | C)) ) );
correctness
existence
ex b1 being set ex L being T-Sequence st
( b1 = last L & dom L = succ A & L . {} = FinSETS & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = Tarski-Class (L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = Universe_closure (Union (L | C)) ) );
uniqueness
for b1, b2 being set st ex L being T-Sequence st
( b1 = last L & dom L = succ A & L . {} = FinSETS & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = Tarski-Class (L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = Universe_closure (Union (L | C)) ) ) & ex L being T-Sequence st
( b2 = last L & dom L = succ A & L . {} = FinSETS & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = Tarski-Class (L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = Universe_closure (Union (L | C)) ) ) holds
b1 = b2;
proof
thus  ( ex x being set ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = FinSETS & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H3(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = H4(C,L | C) ) ) & ( for x1, x2 being set st ex L being T-Sequence st
( x1 = last L & dom L = succ A & L . {} = FinSETS & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H3(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = H4(C,L | C) ) ) & ex L being T-Sequence st
( x2 = last L & dom L = succ A & L . {} = FinSETS & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H3(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = H4(C,L | C) ) ) holds
x1 = x2 ) ) from ORDINAL2:sch_7(); ::_thesis: verum
end;
end;

:: deftheorem Def5 defines UNIVERSE CLASSES2:def_5_:_
 for A being Ordinal
for b2 being set holds
( b2 = UNIVERSE A iff ex L being T-Sequence st
( b2 = last L & dom L = succ A & L . {} = FinSETS & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = Tarski-Class (L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = Universe_closure (Union (L | C)) ) ) );

deffunc H5( Ordinal) ->  set = UNIVERSE $1;

Lm6: now__::_thesis:_(_H5(_{}_)_=_FinSETS_&_(_for_A_being_Ordinal_holds_H5(_succ_A)_=_H3(A,H5(A))_)_&_(_for_A_being_Ordinal
for_L_being_T-Sequence_st_A_<>_{}_&_A_is_limit_ordinal_&_dom_L_=_A_&_(_for_B_being_Ordinal_st_B_in_A_holds_
L_._B_=_H5(B)_)_holds_
H5(A)_=_H4(A,L)_)_)
A1: for A being Ordinal
for x being set holds
( x = H5(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = FinSETS & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H3(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = H4(C,L | C) ) ) ) by Def5;
thus  H5( {} ) = FinSETS from ORDINAL2:sch_8(A1); ::_thesis: ( ( for A being Ordinal holds H5( succ A) = H3(A,H5(A)) ) & ( for A being Ordinal
for L being T-Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = H5(B) ) holds
H5(A) = H4(A,L) ) )
thus  for A being Ordinal holds H5( succ A) = H3(A,H5(A)) from ORDINAL2:sch_9(A1); ::_thesis: for A being Ordinal
for L being T-Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = H5(B) ) holds
H5(A) = H4(A,L)
let A be Ordinal; ::_thesis: for L being T-Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = H5(B) ) holds
H5(A) = H4(A,L)
let L be T-Sequence; ::_thesis: ( A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = H5(B) ) implies H5(A) = H4(A,L) )
assume that
A2: ( A <> {} & A is limit_ordinal ) and
A3: dom L = A and
A4: for B being Ordinal st B in A holds
L . B = H5(B) ; ::_thesis: H5(A) = H4(A,L)
thus  H5(A) = H4(A,L) from ORDINAL2:sch_10(A1, A2, A3, A4); ::_thesis: verum
end;

registration
let A be Ordinal;
cluster UNIVERSE A ->  non empty universal ;
coherence
 ( UNIVERSE A is universal & not UNIVERSE A is empty )
proof
defpred S2[ Ordinal] means  UNIVERSE A is Universe;
A1: for B being Ordinal st S2[B] holds
S2[ succ B]
proof
let B be Ordinal; ::_thesis: ( S2[B] implies S2[ succ B] )
assume  S2[B] ; ::_thesis: S2[ succ B]
then reconsider UU = UNIVERSE B as Universe ;
 UNIVERSE (succ B) = Tarski-Class UU by Lm6;
hence  S2[ succ B] ; ::_thesis: verum
end;
A2: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S2[B] ) holds
S2[A]
proof
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S2[B] ) implies S2[A] )
assume that
A3: A <> {} and
A4: A is limit_ordinal and
 for B being Ordinal st B in A holds
S2[B] ; ::_thesis: S2[A]
consider L being T-Sequence such that
A5: ( dom L = A & ( for B being Ordinal st B in A holds
L . B = H5(B) ) ) from ORDINAL2:sch_2();
UNIVERSE A = Universe_closure (Union L) by A3, A4, A5, Lm6
.= Universe_closure (union (rng L)) by CARD_3:def_4 ;
hence  S2[A] ; ::_thesis: verum
end;
A6: S2[ {} ] by Lm6;
 for A being Ordinal holds S2[A] from ORDINAL2:sch_1(A6, A1, A2);
hence  ( UNIVERSE A is universal & not UNIVERSE A is empty ) ; ::_thesis: verum
end;
end;

theorem :: CLASSES2:65
UNIVERSE {} = FinSETS by Lm6;

theorem :: CLASSES2:66
for A being Ordinal holds UNIVERSE (succ A) = Tarski-Class (UNIVERSE A) by Lm6;

Lm7:  1 = succ 0
;

theorem :: CLASSES2:67
UNIVERSE 1 = SETS by Lm6, Lm7;

theorem :: CLASSES2:68
for A being Ordinal
for L being T-Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = UNIVERSE B ) holds
UNIVERSE A = Universe_closure (Union L) by Lm6;

theorem :: CLASSES2:69
for U being Universe holds
( FinSETS c= U & Tarski-Class {} c= U & UNIVERSE {} c= U )
proof
let U be Universe; ::_thesis: ( FinSETS c= U & Tarski-Class {} c= U & UNIVERSE {} c= U )
A1: On U c= Rank (On U) by CLASSES1:38;
A2: Rank (On U) = U by Th50;
 {} in On U by Th51, ORDINAL3:8;
hence  ( FinSETS c= U & Tarski-Class {} c= U & UNIVERSE {} c= U ) by A2, A1, Lm6, Th4; ::_thesis: verum
end;

theorem Th70: :: CLASSES2:70
for A, B being Ordinal holds
( A in B iff UNIVERSE A in UNIVERSE B )
proof
let A, B be Ordinal; ::_thesis: ( A in B iff UNIVERSE A in UNIVERSE B )
defpred S2[ Ordinal] means  for A being Ordinal st A in $1 holds
UNIVERSE A in UNIVERSE $1;
A1: for B being Ordinal st S2[B] holds
S2[ succ B]
proof
let B be Ordinal; ::_thesis: ( S2[B] implies S2[ succ B] )
assume A2: S2[B] ; ::_thesis: S2[ succ B]
let A be Ordinal; ::_thesis: ( A in succ B implies UNIVERSE A in UNIVERSE (succ B) )
assume A3: A in succ B ; ::_thesis: UNIVERSE A in UNIVERSE (succ B)
 ( A c< B iff ( A c= B & A <> B ) ) by XBOOLE_0:def_8;
then  ( A in B or A = B ) by A3, ORDINAL1:11, ORDINAL1:22;
then A4: ( UNIVERSE A in UNIVERSE B or UNIVERSE A = UNIVERSE B ) by A2;
 UNIVERSE (succ B) = Tarski-Class (UNIVERSE B) by Lm6;
then  UNIVERSE B in UNIVERSE (succ B) by CLASSES1:2;
hence  UNIVERSE A in UNIVERSE (succ B) by A4, ORDINAL1:10; ::_thesis: verum
end;
A5: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S2[B] ) holds
S2[A]
proof
let B be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal & ( for B being Ordinal st B in B holds
S2[B] ) implies S2[B] )
assume that
A6: B <> {} and
A7: B is limit_ordinal and
 for C being Ordinal st C in B holds
for A being Ordinal st A in C holds
UNIVERSE A in UNIVERSE C ; ::_thesis: S2[B]
let A be Ordinal; ::_thesis: ( A in B implies UNIVERSE A in UNIVERSE B )
consider L being T-Sequence such that
A8: ( dom L = B & ( for C being Ordinal st C in B holds
L . C = H5(C) ) ) from ORDINAL2:sch_2();
assume  A in B ; ::_thesis: UNIVERSE A in UNIVERSE B
then A9: succ A in B by A7, ORDINAL1:28;
then  L . (succ A) = UNIVERSE (succ A) by A8;
then  UNIVERSE (succ A) in rng L by A9, A8, FUNCT_1:def_3;
then A10: UNIVERSE (succ A) c= union (rng L) by ZFMISC_1:74;
UNIVERSE B = Universe_closure (Union L) by A6, A7, A8, Lm6
.= Universe_closure (union (rng L)) by CARD_3:def_4 ;
then  union (rng L) c= UNIVERSE B by Def4;
then A11: UNIVERSE (succ A) c= UNIVERSE B by A10, XBOOLE_1:1;
A12: UNIVERSE A in Tarski-Class (UNIVERSE A) by CLASSES1:2;
 UNIVERSE (succ A) = Tarski-Class (UNIVERSE A) by Lm6;
hence  UNIVERSE A in UNIVERSE B by A12, A11; ::_thesis: verum
end;
A13: S2[ {} ] ;
A14: for B being Ordinal holds S2[B] from ORDINAL2:sch_1(A13, A1, A5);
hence  ( A in B implies UNIVERSE A in UNIVERSE B ) ; ::_thesis: ( UNIVERSE A in UNIVERSE B implies A in B )
assume that
A15: UNIVERSE A in UNIVERSE B and
A16: not A in B ; ::_thesis: contradiction
 ( B c< A iff ( B c= A & B <> A ) ) by XBOOLE_0:def_8;
then  ( B in A or B = A ) by A16, ORDINAL1:11, ORDINAL1:16;
hence  contradiction by A14, A15; ::_thesis: verum
end;

theorem :: CLASSES2:71
for A, B being Ordinal st UNIVERSE A = UNIVERSE B holds
A = B
proof
let A, B be Ordinal; ::_thesis: ( UNIVERSE A = UNIVERSE B implies A = B )
assume that
A1: UNIVERSE A = UNIVERSE B and
A2: A <> B ; ::_thesis: contradiction
 ( A in B or B in A ) by A2, ORDINAL1:14;
then  ( UNIVERSE A in UNIVERSE B or UNIVERSE B in UNIVERSE A ) by Th70;
hence  contradiction by A1; ::_thesis: verum
end;

theorem :: CLASSES2:72
for A, B being Ordinal holds
( A c= B iff UNIVERSE A c= UNIVERSE B )
proof
let A, B be Ordinal; ::_thesis: ( A c= B iff UNIVERSE A c= UNIVERSE B )
thus  ( A c= B implies UNIVERSE A c= UNIVERSE B ) ::_thesis: ( UNIVERSE A c= UNIVERSE B implies A c= B )
proof
assume A1: A c= B ; ::_thesis: UNIVERSE A c= UNIVERSE B
assume  not UNIVERSE A c= UNIVERSE B ; ::_thesis: contradiction
then  UNIVERSE B in UNIVERSE A by Th53;
then  B in A by Th70;
hence  contradiction by A1, ORDINAL1:5; ::_thesis: verum
end;
assume A2: UNIVERSE A c= UNIVERSE B ; ::_thesis: A c= B
assume  not A c= B ; ::_thesis: contradiction
then  B in A by ORDINAL1:16;
then  UNIVERSE B in UNIVERSE A by Th70;
hence  contradiction by A2, ORDINAL1:5; ::_thesis: verum
end;


theorem :: CLASSES2:73
for X being set holds
( Tarski-Class (X,{}) in Tarski-Class (X,1) & Tarski-Class (X,{}) <> Tarski-Class (X,1) )
proof
let X be set ; ::_thesis: ( Tarski-Class (X,{}) in Tarski-Class (X,1) & Tarski-Class (X,{}) <> Tarski-Class (X,1) )
deffunc H6( Ordinal) ->  Element of bool (Tarski-Class X) = Tarski-Class (X,$1);
deffunc H7( Ordinal, set ) ->  set = ( {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in $2 & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in $2  }  ) \/ ((bool $2) /\ (Tarski-Class X));
deffunc H8( Ordinal, T-Sequence) ->  set = (union (rng $2)) /\ (Tarski-Class X);
A1: for A being Ordinal
for x being set holds
( x = H6(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H7(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = H8(C,L | C) ) ) ) by CLASSES1:def_5;
A2: H6( {} ) = {X} from ORDINAL2:sch_8(A1);
then  X in Tarski-Class (X,{}) by TARSKI:def_1;
then A3: bool X in Tarski-Class X by CLASSES1:4;
 {X} c= bool X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {X} or x in bool X )
assume  x in {X} ; ::_thesis: x in bool X
then  x = X by TARSKI:def_1;
hence  x in bool X by ZFMISC_1:def_1; ::_thesis: verum
end;
then  ( 1 = succ 0 & {X} in Tarski-Class X ) by A3, CLASSES1:3;
hence A4: Tarski-Class (X,{}) in Tarski-Class (X,1) by A2, CLASSES1:10; ::_thesis: Tarski-Class (X,{}) <> Tarski-Class (X,1)
assume  Tarski-Class (X,{}) = Tarski-Class (X,1) ; ::_thesis: contradiction
hence  contradiction by A4; ::_thesis: verum
end;