The Mizar article:

Tarski's Classes and Ranks

by
Grzegorz Bancerek

Received March 23, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: CLASSES1
[ MML identifier index ]


environ

 vocabulary FUNCT_1, TARSKI, SETFAM_1, BOOLE, CARD_1, ORDINAL1, ORDINAL2,
      RELAT_1, MCART_1, CLASSES1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      NUMBERS, NAT_1, ORDINAL1, MCART_1, ORDINAL2, CARD_1;
 constructors SETFAM_1, NAT_1, MCART_1, WELLORD2, CARD_1, MEMBERED, XBOOLE_0;
 clusters SUBSET_1, ORDINAL1, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements NUMERALS, SUBSET, BOOLE;
 definitions TARSKI, ORDINAL1, WELLORD2, FUNCT_1, XBOOLE_0;
 theorems TARSKI, SETFAM_1, ZFMISC_1, ORDINAL1, MCART_1, ORDINAL2, FUNCT_1,
      CARD_1, WELLORD2, ENUMSET1, XBOOLE_0, XBOOLE_1;
 schemes ORDINAL1, ORDINAL2, TARSKI, PARTFUN1, NAT_1, RECDEF_1, XBOOLE_0;

begin

 reserve W,X,Y,Z for set,
         f,g for Function,
         a,x,y,z for set;

definition let B be set;
 attr B is subset-closed means
:Def1: for X,Y holds X in B & Y c= X implies Y in B;
end;

definition let B be set;
 attr B is being_Tarski-Class means
:Def2:  B is subset-closed &
       (for X holds X in B implies bool X in B) &
       (for X holds X c= B implies X,B are_equipotent or X in B);
  synonym B is_Tarski-Class;
end;

definition let A,B be set;
 pred B is_Tarski-Class_of A means
:Def3: A in B & B is_Tarski-Class;
end;

definition let A be set;
 func Tarski-Class A -> set means
:Def4: it is_Tarski-Class_of A &
     for D being set st D is_Tarski-Class_of A holds it c= D;
  existence
   proof
    consider Big being set such that
A1:   A in Big &
     (for X,Y holds X in Big & Y c= X implies Y in Big) &
     (for X holds X in Big implies bool X in Big) &
     (for X holds X c= Big implies X,Big are_equipotent or X in Big)
     by ZFMISC_1:136;
       Big is subset-closed by A1,Def1;
then A2:  Big is_Tarski-Class by A1,Def2;
defpred P[set] means $1 is_Tarski-Class_of A;
    consider Classes being set such that
A3:   X in Classes iff X in bool Big & P[X] from Separation;
    set IT = meet Classes;
A4: Big in bool Big & Big is_Tarski-Class_of A by A1,A2,Def3,ZFMISC_1:def 1;
then A5:  Big in Classes by A3;
A6:     Classes <> {} by A3,A4;
A7:     now let X; assume X in Classes;
       then X is_Tarski-Class_of A by A3;
      hence A in X by Def3;
     end;
then A8:   A in IT by A6,SETFAM_1:def 1;
    take IT;
    thus A in IT by A6,A7,SETFAM_1:def 1;
    thus
A9:  X in IT & Y c= X implies Y in IT
      proof assume
A10:     X in IT & Y c= X;
          now let Z; assume
A11:       Z in Classes;
          then Z is_Tarski-Class_of A by A3;
          then Z is_Tarski-Class by Def3;
          then Z is subset-closed by Def2;
          then (for X,Y holds X in Z & Y c= X implies Y in Z) & X in Z
           by A10,A11,Def1,SETFAM_1:def 1;
         hence Y in Z by A10;
        end;
       hence Y in IT by A6,SETFAM_1:def 1;
      end;
    thus
A12:  X in IT implies bool X in IT
      proof assume
A13:     X in IT;
          now let Z; assume
A14:       Z in Classes;
          then Z is_Tarski-Class_of A by A3;
          then Z is_Tarski-Class by Def3;
          then (for X holds X in Z implies bool X in Z) & X in Z
           by A13,A14,Def2,SETFAM_1:def 1;
         hence bool X in Z;
        end;
       hence bool X in IT by A6,SETFAM_1:def 1;
      end;
    thus
A15:  X c= IT implies X,IT are_equipotent or X in IT
      proof assume that
A16:     X c= IT and
A17:     not X,IT are_equipotent;
          now let Z; assume
A18:       Z in Classes;
          then Z is_Tarski-Class_of A by A3;
then A19:          Z is_Tarski-Class by Def3;
A20:       IT c= Z by A18,SETFAM_1:4;
          then X c= Z by A16,XBOOLE_1:1;
       then X,Z are_equipotent or X in Z by A19,Def2;
         hence X in Z by A16,A17,A20,CARD_1:44;
        end;
       hence X in IT by A6,SETFAM_1:def 1;
      end;
    let D be set; assume
    D is_Tarski-Class_of A;
then A21:   A in D & D is_Tarski-Class by Def3;
then A22: D is subset-closed by Def2;
A23:   IT /\ D is_Tarski-Class_of A
      proof
       thus A in IT /\ D by A8,A21,XBOOLE_0:def 3;
       thus X in IT /\ D & Y c= X implies Y in IT /\ D
         proof assume
A24:        X in IT /\ D & Y c= X;
           then X in IT & X in D by XBOOLE_0:def 3;
           then Y in IT & Y in D by A9,A22,A24,Def1;
          hence Y in IT /\ D by XBOOLE_0:def 3;
         end;
       thus X in IT /\ D implies bool X in IT /\ D
         proof assume X in IT /\ D;
           then X in IT & X in D by XBOOLE_0:def 3;
           then bool X in IT & bool X in D by A12,A21,Def2;
          hence bool X in IT /\ D by XBOOLE_0:def 3;
         end;
       let X such that
A25:     X c= IT /\ D and
A26:     not X,IT /\ D are_equipotent;
A27:     IT /\ D c= IT & IT /\ D c= D by XBOOLE_1:17;
then A28:     X c= IT & X c= D by A25,XBOOLE_1:1;
          not X,IT are_equipotent & not X,D are_equipotent
        by A25,A26,A27,CARD_1:44;
        then X in IT & X in D by A15,A21,A28,Def2;
       hence X in IT /\ D by XBOOLE_0:def 3;
      end;
       IT /\ D c= Big
      proof let x; assume x in IT /\ D;
        then x in IT by XBOOLE_0:def 3;
       hence x in Big by A5,SETFAM_1:def 1;
      end;
     then IT /\ D in Classes by A3,A23;
     then IT c= IT /\ D & IT /\ D c= D by SETFAM_1:4,XBOOLE_1:17;
    hence thesis by XBOOLE_1:1;
   end;
  uniqueness
   proof let D1,D2 be set such that
A29:  D1 is_Tarski-Class_of A &
      for D being set st D is_Tarski-Class_of A holds D1 c= D and
A30:  D2 is_Tarski-Class_of A &
      for D being set st D is_Tarski-Class_of A holds D2 c= D;
    thus D1 c= D2 & D2 c= D1 by A29,A30;
   end;
end;

definition let A be set;
 cluster Tarski-Class A -> non empty;
coherence
 proof
      Tarski-Class A is_Tarski-Class_of A by Def4; hence thesis by Def3;
 end;
end;

canceled;

theorem
   W is_Tarski-Class iff
   W is subset-closed &
   (for X st X in W holds bool X in W) &
   (for X st X c= W & Card X <` Card W holds X in W)
  proof
  hereby assume
A1: W is_Tarski-Class;
   hence W is subset-closed &
    for X st X in W holds bool X in W by Def2;
   let X;
   assume
A2: X c= W & Card X <` Card W;
    then Card X <> Card W;
    then not X,W are_equipotent by CARD_1:21;
   hence X in W by A1,A2,Def2;
  end;
    now assume
A3:    for X st X c= W & Card X <` Card W holds X in W;
     let X; assume X c= W;
      then Card X <=` Card W & not Card X <` Card W or X in W by A3,CARD_1:27;
      then Card X = Card W or X in W by CARD_1:13;
     hence X,W are_equipotent or X in W by CARD_1:21;
    end;
   hence thesis by Def2;
  end;

canceled 2;

theorem
 Th5: X in Tarski-Class X
  proof Tarski-Class X is_Tarski-Class_of X by Def4;
   hence thesis by Def3;
  end;

theorem
 Th6: Y in Tarski-Class X & Z c= Y implies Z in Tarski-Class X
  proof
    Tarski-Class X is_Tarski-Class_of X by Def4;
    then Tarski-Class X is_Tarski-Class by Def3;
    then Tarski-Class X is subset-closed by Def2;
   hence thesis by Def1;
  end;

theorem
 Th7: Y in Tarski-Class X implies bool Y in Tarski-Class X
  proof Tarski-Class X is_Tarski-Class_of X by Def4;
    then Tarski-Class X is_Tarski-Class by Def3;
   hence thesis by Def2;
  end;

theorem
 Th8: Y c= Tarski-Class X implies
      Y,Tarski-Class X are_equipotent or Y in Tarski-Class X
  proof Tarski-Class X is_Tarski-Class_of X by Def4;
    then Tarski-Class X is_Tarski-Class by Def3;
   hence thesis by Def2;
  end;

theorem
    Y c= Tarski-Class X & Card Y <` Card Tarski-Class X implies
   Y in Tarski-Class X
  proof assume
A1:  Y c= Tarski-Class X & Card Y <` Card Tarski-Class X;
    then Card Y <> Card Tarski-Class X;
    then not Y,Tarski-Class X are_equipotent by CARD_1:21;
   hence thesis by A1,Th8;
  end;

 reserve u,v for Element of Tarski-Class(X),
         A,B,C for Ordinal,
         L,L1 for T-Sequence;

definition let X,A;
 func Tarski-Class(X,A) means
:Def5:
   ex L st it = last L & dom L = succ A & L.{} = { X } &
    (for C st succ C in succ A holds
     L.succ C = { u : ex v st v in L.C & u c= v } \/
                { bool v : v in L.C } \/
                bool(L.C) /\ Tarski-Class X) &
      for C st C in succ A & C <> {} & C is_limit_ordinal
             holds L.C = (union rng(L|C)) /\ Tarski-Class X;
  correctness
proof
  deffunc C(Ordinal,set) = { u : ex v st v in $2 & u c= v } \/
                { bool v : v in $2 } \/
                bool $2 /\ Tarski-Class X;
  deffunc D(Ordinal,T-Sequence) = (union rng $2) /\ Tarski-Class X;
  thus (ex x,L st x = last L & dom L = succ A & L.{} = {X} &
     (for C st succ C in succ A holds L.succ C = C(C,L.C)) &
      for C st C in succ A & C <> {} & C is_limit_ordinal
             holds L.C = D(C,L|C) ) &
   for x1,x2 being set st
    (ex L st x1 = last L & dom L = succ A & L.{} = {X} &
      (for C st succ C in succ A holds L.succ C = C(C,L.C)) &
       for C st C in succ A & C <> {} & C is_limit_ordinal
              holds L.C = D(C,L|C) ) &
    (ex L st x2 = last L & dom L = succ A & L.{} = {X} &
      (for C st succ C in succ A holds L.succ C = C(C,L.C)) &
       for C st C in succ A & C <> {} & C is_limit_ordinal
              holds L.C = D(C,L|C) )
     holds x1 = x2 from TS_Def;
  end;
end;

Lm1:
 now let X;
   deffunc F(Ordinal) = Tarski-Class(X,$1);
   deffunc C(Ordinal,set) = { u : ex v st v in $2 & u c= v } \/
                 { bool v : v in $2 } \/
                 bool $2 /\ Tarski-Class X;
   deffunc D(Ordinal,T-Sequence) = (union rng $2) /\ Tarski-Class X;
A1: for A,x holds x = F(A) iff
    ex L st x = last L & dom L = succ A & L.{} = { X } &
     (for C st succ C in succ A holds L.succ C = C(C,L.C)) &
      for C st C in succ A & C <> {} & C is_limit_ordinal
              holds L.C = D(C,L|C) by Def5;
  thus F({}) = { X } from TS_Result0(A1);
  thus for A holds F(succ A) = C(A,F(A)) from TS_ResultS(A1);
  thus A <> {} & A is_limit_ordinal & dom L = A &
     (for B st B in A holds L.B = Tarski-Class(X,B)) implies
      Tarski-Class(X,A) = (union rng L) /\ Tarski-Class X
    proof assume that
A2:    A <> {} & A is_limit_ordinal and
A3:    dom L = A and
A4:    for B st B in A holds L.B = F(B);
     thus F(A) = D(A,L) from TS_ResultL(A1,A2,A3,A4);
    end;
 end;

definition let X,A;
 redefine func Tarski-Class(X,A) -> Subset of Tarski-Class X;
  coherence
   proof
     defpred P[Ordinal] means Tarski-Class(X,$1) is Subset of Tarski-Class X;
     { X } c= Tarski-Class X
      proof let x; assume x in { X };
        then x = X by TARSKI:def 1;
       hence thesis by Th5;
      end;
then A1: P[{}] by Lm1;
A2:   P[B] implies P[succ B]
      proof assume Tarski-Class(X,B) is Subset of Tarski-Class X;
       then reconsider S = Tarski-Class(X,B) as Subset of Tarski-Class X;
       set Y = Tarski-Class(X,succ B);
          Y c= Tarski-Class X
         proof let x; assume x in Y;
           then x in { u : ex v st v in S & u c= v } \/ { bool v : v in S } \/
               bool S /\ Tarski-Class X by Lm1;
then A3:           x in { u : ex v st v in S & u c= v } \/ { bool v : v in S }
or
           x in bool S /\ Tarski-Class X by XBOOLE_0:def 2;
A4:        now assume x in { u : ex v st v in S & u c= v };
             then ex u st x = u & ex v st v in S & u c= v;
            hence thesis;
           end;
          now assume x in { bool v : v in S };
             then ex v st x = bool v & v in S;
            hence thesis by Th7;
           end;
          hence thesis by A3,A4,XBOOLE_0:def 2,def 3;
         end;
       hence thesis;
      end;
A5:   for B st B <> {} & B is_limit_ordinal &
       for C st C in B holds P[C] holds P[B]
      proof let B such that
A6:     B <> {} & B is_limit_ordinal and
          for C st C in B holds Tarski-Class(X,C) is Subset of Tarski-Class X;
        deffunc f(Ordinal) = Tarski-Class(X,$1);
       consider L such that
A7:     dom L = B & for C st C in B holds L.C = f(C) from TS_Lambda;
          Tarski-Class(X,B) = (union rng L) /\ Tarski-Class X &
         (union rng L) /\ Tarski-Class X c= Tarski-Class X
          by A6,A7,Lm1,XBOOLE_1:17;
       hence thesis;
      end;
      for A holds P[A] from Ordinal_Ind(A1,A2,A5);
    hence thesis;
   end;
end;

theorem
   Tarski-Class(X,{}) = { X } by Lm1;

theorem
   Tarski-Class(X,succ A) =
      { u : ex v st v in Tarski-Class(X,A) & u c= v } \/
      { bool v : v in Tarski-Class(X,A) } \/
      bool Tarski-Class(X,A) /\ Tarski-Class X by Lm1;

theorem
 Th12: A <> {} & A is_limit_ordinal implies
      Tarski-Class(X,A) = { u : ex B st B in A & u in Tarski-Class(X,B) }
  proof assume
A1:  A <> {} & A is_limit_ordinal;
   deffunc f(Ordinal) = Tarski-Class(X,$1);
   consider L such that
A2:  dom L = A & for B st B in A holds L.B = f(B) from TS_Lambda;
A3:  Tarski-Class(X,A) = (union rng L) /\ Tarski-Class X by A1,A2,Lm1;
   thus Tarski-Class(X,A) c= { u : ex B st B in A & u in Tarski-Class(X,B) }
     proof let x; assume x in Tarski-Class(X,A);
       then x in union rng L by A3,XBOOLE_0:def 3;
      then consider Y such that
A4:     x in Y & Y in rng L by TARSKI:def 4;
      consider y such that
A5:     y in dom L & Y = L.y by A4,FUNCT_1:def 5;
      reconsider y as Ordinal by A5,ORDINAL1:23;
         Y = Tarski-Class(X,y) by A2,A5;
       hence thesis by A2,A4,A5;
     end;
   let x; assume x in { u : ex B st B in A & u in Tarski-Class(X,B) };
   then consider u such that
A6:  x = u & ex B st B in A & u in Tarski-Class(X,B);
   consider B such that
A7:  B in A & u in Tarski-Class(X,B) by A6;
      L.B = Tarski-Class(X,B) by A2,A7;
    then Tarski-Class(X,B) in rng L by A2,A7,FUNCT_1:def 5;
    then u in union rng L & u in Tarski-Class X by A7,TARSKI:def 4;
   hence thesis by A3,A6,XBOOLE_0:def 3;
  end;

theorem
 Th13: Y in Tarski-Class(X,succ A) iff
   Y c= Tarski-Class(X,A) & Y in Tarski-Class X or
   ex Z st Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z)
  proof
   set T1 = { u : ex v st v in Tarski-Class(X,A) & u c= v };
   set T2 = { bool v : v in Tarski-Class(X,A) };
   set T3 = bool Tarski-Class(X,A) /\ Tarski-Class X;
A1:  Tarski-Class(X,succ A) = T1 \/ T2 \/ T3 by Lm1;
   thus Y in Tarski-Class(X,succ A) implies
      Y c= Tarski-Class(X,A) & Y in Tarski-Class X or
      ex Z st Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z)
     proof assume
         Y in Tarski-Class(X,succ A);
then A2:       Y in T1 \/ T2 or Y in T3 by A1,XBOOLE_0:def 2;
A3:     now assume Y in T1;
         then ex u st Y = u & ex v st v in Tarski-Class(X,A) & u c= v;
        hence ex Z st Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z);
       end;
A4:     now assume Y in T2;
         then ex v st Y = bool v & v in Tarski-Class(X,A);
        hence ex Z st Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z);
       end;
         now assume Y in T3;
         then Y in bool Tarski-Class(X,A) & Y in Tarski-Class X by XBOOLE_0:def
3;
        hence thesis;
       end;
      hence thesis by A2,A3,A4,XBOOLE_0:def 2;
     end;
   assume
A5:  Y c= Tarski-Class(X,A) & Y in Tarski-Class X or
     ex Z st Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z);
A6:  now assume
     Y c= Tarski-Class(X,A) & Y in Tarski-Class X;
      then Y in T3 by XBOOLE_0:def 3;
     hence Y in Tarski-Class(X,succ A) by A1,XBOOLE_0:def 2;
    end;
      now given Z such that
A7:   Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z);
     reconsider Z as Element of Tarski-Class X by A7;
      reconsider y = Y as Element of Tarski-Class X by A7,Th6,Th7;
A8:   now assume Y c= Z;
        then y in T1 by A7; then Y in T1 \/ T2 by XBOOLE_0:def 2;
       hence thesis by A1,XBOOLE_0:def 2;
      end;
        now assume Y = bool Z;
        then y in T2 by A7; then Y in T1 \/ T2 by XBOOLE_0:def 2;
       hence thesis by A1,XBOOLE_0:def 2;
      end;
     hence thesis by A7,A8;
    end;
   hence thesis by A5,A6;
  end;

theorem
   Y c= Z & Z in Tarski-Class(X,A) implies Y in Tarski-Class(X,succ A) by Th13;

theorem
   Y in Tarski-Class(X,A) implies bool Y in Tarski-Class(X,succ A) by Th13;

theorem
 Th16: A <> {} & A is_limit_ordinal implies
   (x in Tarski-Class(X,A) iff ex B st B in A & x in Tarski-Class(X,B))
  proof assume
A1:  A <> {} & A is_limit_ordinal;
then A2:  Tarski-Class(X,A) = { u : ex B st B in A & u in Tarski-Class(X,B) }
     by Th12;
   thus x in Tarski-Class(X,A) implies ex B st B in A & x in Tarski-Class(X,B)
     proof assume x in Tarski-Class(X,A);
       then ex u st x = u & ex B st B in A & u in Tarski-Class(X,B) by A2;
      hence thesis;
     end;
   given B such that
A3:  B in A & x in Tarski-Class(X,B);
   reconsider u = x as Element of Tarski-Class X by A3;
      u in { v : ex B st B in A & v in Tarski-Class(X,B) } by A3;
   hence thesis by A1,Th12;
  end;

theorem
    A <> {} & A is_limit_ordinal & Y in Tarski-Class(X,A) &
   (Z c= Y or Z = bool Y) implies Z in Tarski-Class(X,A)
  proof assume
A1:  A <> {} & A is_limit_ordinal & Y in Tarski-Class(X,A);
   then consider B such that
A2:  B in A & Y in Tarski-Class(X,B) by Th16;
A3:  bool Y in Tarski-Class(X,succ B) by A2,Th13;
A4:  Z c= Y implies Z in Tarski-Class(X,succ B) by A2,Th13;
A5:  succ B in A by A1,A2,ORDINAL1:41;
   assume Z c= Y or Z = bool Y;
   hence thesis by A1,A3,A4,A5,Th16;
  end;

theorem
 Th18: Tarski-Class(X,A) c= Tarski-Class(X,succ A)
  proof let x; assume
   x in Tarski-Class(X,A);
    then x in { u : ex v st v in Tarski-Class(X,A) & u c= v };
then A1:  x in { u : ex v st v in Tarski-Class(X,A) & u c= v } \/
        { bool v : v in Tarski-Class(X,A) } by XBOOLE_0:def 2;
      Tarski-Class(X,succ A) =
      { u : ex v st v in Tarski-Class(X,A) & u c= v } \/
      { bool v : v in Tarski-Class(X,A) } \/
      bool Tarski-Class(X,A) /\ Tarski-Class X by Lm1;
   hence thesis by A1,XBOOLE_0:def 2;
  end;

theorem
 Th19: A c= B implies Tarski-Class(X,A) c= Tarski-Class(X,B)
  proof
   defpred OnP[Ordinal] means
    A c= $1 implies Tarski-Class(X,A) c= Tarski-Class(X,$1);
A1:for B st for C st C in B holds OnP[C] holds OnP[B]
     proof let B such that
A2:     for C st C in B holds OnP[C] and
A3:     A c= B;
      let x; assume
A4:     x in Tarski-Class(X,A);
         now assume A5: A <> B;
          then A c< B by A3,XBOOLE_0:def 8;
then A6:       A in B by ORDINAL1:21;
            A c= B & B <> A iff A c< B by XBOOLE_0:def 8;
then A7:       B <> {} by A3,A5,ORDINAL1:21;
A8:       now given C such that
A9:        B = succ C;
          A c= C & C in B by A6,A9,ORDINAL1:34;
           then Tarski-Class(X,A) c= Tarski-Class(X,C) &
            Tarski-Class(X,C) c= Tarski-Class(X,B) by A2,A9,Th18;
           then Tarski-Class(X,A) c= Tarski-Class(X,B) by XBOOLE_1:1;
          hence thesis by A4;
         end;
           now assume for C holds B <> succ C;
           then B is_limit_ordinal by ORDINAL1:42;
       then Tarski-Class(X,B) = { v : ex C st C in B & v in Tarski-Class(X,C) }
             by A7,Th12;
           hence thesis by A4,A6;
         end;
        hence thesis by A8;
       end;
      hence thesis by A4;
     end;
      for B holds OnP[B] from Transfinite_Ind(A1);
   hence thesis;
  end;

theorem
 Th20: ex A st Tarski-Class(X,A) = Tarski-Class(X,succ A)
  proof assume
A1:  for A holds Tarski-Class(X,A) <> Tarski-Class(X,succ A);
defpred P[set] means ex A st $1 in Tarski-Class(X,A);
   consider Z such that
A2:  x in Z iff x in Tarski-Class X & P[x] from Separation;
   defpred P[set,set] means
    ex A st $2 = A & $1 in Tarski-Class(X,succ A) & not $1 in
 Tarski-Class(X,A);
A3:  for x,y,z st P[x,y] & P[x,z] holds y = z
     proof let x,y,z;
      given A such that
A4:    y = A & x in Tarski-Class(X,succ A) & not x in Tarski-Class(X,A);
      given B such that
A5:    z = B & x in Tarski-Class(X,succ B) & not x in Tarski-Class(X,B);
      assume A6: y <> z;
      A c= B or B c= A;
then A7:     A c< B or B c< A by A4,A5,A6,XBOOLE_0:def 8;
         now assume A c< B;
         then A in B by ORDINAL1:21;
         then succ A c= B by ORDINAL1:33;
         then Tarski-Class(X,succ A) c= Tarski-Class(X,B) by Th19;
        hence contradiction by A4,A5;
       end;
       then B in A by A7,ORDINAL1:21;
       then succ B c= A by ORDINAL1:33;
       then Tarski-Class(X,succ B) c= Tarski-Class(X,A) by Th19;
      hence contradiction by A4,A5;
     end;
   consider Y such that
A8:  x in Y iff ex y st y in Z & P[y,x] from Fraenkel(A3);
      now let A;
A9:    Tarski-Class(X,A) <> Tarski-Class(X,succ A) &
       Tarski-Class(X,A) c= Tarski-Class(X,succ A) by A1,Th18;
     then consider x such that
A10: not (x in Tarski-Class(X,A) iff x in Tarski-Class(X,succ A)) by TARSKI:2;
        x in Z by A2,A10;
     hence A in Y by A8,A9,A10;
    end;
   hence contradiction by ORDINAL1:38;
  end;

theorem
 Th21: Tarski-Class(X,A) = Tarski-Class(X,succ A) implies
   Tarski-Class(X,A) = Tarski-Class X
  proof assume
A1:  Tarski-Class(X,A) = Tarski-Class(X,succ A);
      {} = {} & {} c= A by XBOOLE_1:2;
then A2:    Tarski-Class(X,{}) c= Tarski-Class(X,A) &
     Tarski-Class(X,{}) = { X } & X in { X }
      by Lm1,Th19,TARSKI:def 1;
      Tarski-Class(X,A) is_Tarski-Class_of X
     proof
      thus X in Tarski-Class(X,A) by A2;
A3:     Tarski-Class(X,succ A) =
        { u : ex v st v in Tarski-Class(X,A) & u c= v } \/
        { bool v : v in Tarski-Class(X,A) } \/
        bool Tarski-Class(X,A) /\ Tarski-Class X by Lm1;
         Tarski-Class X is_Tarski-Class_of X by Def4;
then A4:       Tarski-Class X is_Tarski-Class by Def3;
      thus Z in Tarski-Class(X,A) & Y c= Z implies Y in Tarski-Class(X,A)
        proof assume
A5:        Z in Tarski-Class(X,A) & Y c= Z;
           Tarski-Class X is_Tarski-Class_of X by Def4;
         then Tarski-Class X is_Tarski-Class by Def3;
         then Tarski-Class X is subset-closed by Def2;
         then reconsider y = Y as Element of Tarski-Class X
            by A5,Def1;
            ex v st v in Tarski-Class(X,A) & y c= v by A5;
          then Y in { u : ex v st v in Tarski-Class(X,A) & u c= v };
          then Y in { u : ex v st v in Tarski-Class(X,A) & u c= v } \/
              { bool v : v in Tarski-Class(X,A) } by XBOOLE_0:def 2;
         hence Y in Tarski-Class(X,A) by A1,A3,XBOOLE_0:def 2;
        end;
      thus Y in Tarski-Class(X,A) implies bool Y in Tarski-Class(X,A)
        proof assume
          Y in Tarski-Class(X,A);
          then bool Y in { bool u : u in Tarski-Class(X,A) };
          then bool Y in { u : ex v st v in Tarski-Class(X,A) & u c= v } \/
                   { bool v : v in Tarski-Class(X,A) } by XBOOLE_0:def 2;
         hence bool Y in Tarski-Class(X,A) by A1,A3,XBOOLE_0:def 2;
        end;
      let Y; assume that
A6:     Y c= Tarski-Class(X,A) and
A7:     not Y,Tarski-Class(X,A) are_equipotent;
         Y c= Tarski-Class X by A6,XBOOLE_1:1;
     then Y,Tarski-Class X are_equipotent or Y in Tarski-Class X by A4,Def2;
      hence Y in Tarski-Class(X,A) by A1,A6,A7,Th13,CARD_1:44;
     end; hence Tarski-Class(X,A) c= Tarski-Class X &
     Tarski-Class X c= Tarski-Class(X,A) by Def4;
  end;

theorem
 Th22: ex A st Tarski-Class(X,A) = Tarski-Class X
  proof
   consider A such that
A1:  Tarski-Class(X,A) = Tarski-Class(X,succ A) by Th20;
   take A;
   thus thesis by A1,Th21;
  end;

theorem
    ex A st Tarski-Class(X,A) = Tarski-Class X &
    for B st B in A holds Tarski-Class(X,B) <> Tarski-Class X
  proof
    defpred P[Ordinal] means Tarski-Class(X,$1) = Tarski-Class X;
A1:  ex A st P[A] by Th22;
   consider A such that
A2:  P[A] & for B st P[B] holds A c= B from Ordinal_Min(A1);
   take A;
   thus Tarski-Class(X,A) = Tarski-Class X by A2;
   let B; assume B in A;
    then not A c= B by ORDINAL1:7;
   hence thesis by A2;
  end;

theorem
    Y <> X & Y in Tarski-Class X implies
   ex A st not Y in Tarski-Class(X,A) & Y in Tarski-Class(X,succ A)
  proof assume
A1:  Y <> X & Y in Tarski-Class X;
     defpred P[Ordinal] means Y in Tarski-Class(X,$1);
      ex A st Tarski-Class(X,A) = Tarski-Class X by Th22;
then A2:  ex A st P[A] by A1;
   consider A such that
A3:  P[A] & for B st P[B] holds A c= B from Ordinal_Min(A2);
A4:    not Y in { X } & Tarski-Class(X,{}) = { X } by A1,Lm1,TARSKI:def 1;
      now assume A is_limit_ordinal;
     then consider B such that
A5:    B in A & Y in Tarski-Class(X,B) by A3,A4,Th16;
        A c= B by A3,A5;
     hence contradiction by A5,ORDINAL1:7;
    end;
   then consider B such that
A6:  A = succ B by ORDINAL1:42;
   take B;
      B in A by A6,ORDINAL1:10;
    then not A c= B by ORDINAL1:7;
   hence thesis by A3,A6;
  end;

theorem
 Th25: X is epsilon-transitive implies
   for A st A <> {} holds Tarski-Class(X,A) is epsilon-transitive
  proof assume
A1:  Y in X implies Y c= X;
   defpred OnP[Ordinal] means
    $1 <> {} implies Tarski-Class(X,$1) is epsilon-transitive;
A2:for A st for B st B in A holds OnP[B] holds OnP[A]
     proof let A such that
A3:     for B st B in A holds OnP[B] and
A4:     A <> {};
      let Y such that
A5:     Y in Tarski-Class(X,A);
A6:     now given B such that
A7:      A = succ B;
           B in A by A7,ORDINAL1:10;
then A8:      B c= A & OnP[B] by A3,ORDINAL1:def 2;
then A9:      Tarski-Class(X,B) c= Tarski-Class(X,A) by Th19;
           now assume not Y c= Tarski-Class(X,B);
          then consider Z such that
A10:        Z in Tarski-Class(X,B) & (Y c= Z or Y = bool Z) by A5,A7,Th13;
A11:        now assume
A12:          Y = bool Z;
            thus thesis
              proof let x;
               assume x in Y;
               hence thesis by A7,A10,A12,Th13;
              end;
           end;
             now assume
A13:          Y c= Z;
            thus thesis
              proof let x; assume A14: x in Y;
then A15:             x in Z by A13;
A16:             now assume B = {};
                  then Tarski-Class(X,B) = { X } by Lm1;
then A17:               Z = X by A10,TARSKI:def 1;
                  then x c= X by A1,A13,A14;
                 hence x in Tarski-Class(X,A) by A7,A10,A17,Th13;
                end;
                  now assume B <> {};
                  then Z c= Tarski-Class(X,B) by A8,A10,ORDINAL1:def 2;
                  then x in Tarski-Class(X,B) by A15;
                 hence thesis by A9;
                end;
               hence thesis by A16;
              end;
           end;
          hence thesis by A10,A11;
         end;
        hence thesis by A9,XBOOLE_1:1;
       end;
         now assume
A18:       for B holds A <> succ B;
         then A is_limit_ordinal by ORDINAL1:42;
        then consider B such that
A19:       B in A & Y in Tarski-Class(X,B) by A4,A5,Th16;
A20:      succ B c= A & succ B <> A & succ B <> {} &
          Tarski-Class(X,B) c= Tarski-Class(X,succ B)
           by A18,A19,Th18,ORDINAL1:33;
           then succ B c< A by XBOOLE_0:def 8;
then A21:       succ B in A & succ B <> {} & Y in Tarski-Class(X,succ B) &
          Tarski-Class(X,succ B) c= Tarski-Class(X,A)
           by A19,A20,Th19,ORDINAL1:21;
         then Tarski-Class(X,succ B) is epsilon-transitive by A3;
         then Y c= Tarski-Class(X,succ B) by A19,A20,ORDINAL1:def 2;
        hence thesis by A21,XBOOLE_1:1;
       end;
      hence thesis by A6;
     end;
   thus for A holds OnP[A] from Transfinite_Ind(A2);
  end;

theorem
    Tarski-Class(X,{}) in Tarski-Class(X,one) &
   Tarski-Class(X,{}) <> Tarski-Class(X,one)
  proof
A1:  Tarski-Class(X,{}) = { X } by Lm1;
    then X in Tarski-Class(X,{}) by TARSKI:def 1;
then A2:  bool X in Tarski-Class X by Th7;
      { X } c= bool X
     proof let a; assume a in { X }; then a = X by TARSKI:def 1;
      hence a in bool X by ZFMISC_1:def 1;
     end;
  then { X } in Tarski-Class X by A2,Th6;
   hence
A3:  Tarski-Class(X,{}) in Tarski-Class(X,one) by A1,Th13,ORDINAL2:def 4;
   assume Tarski-Class(X,{}) = Tarski-Class(X,one);
   hence contradiction by A3;
  end;

theorem
 Th27: X is epsilon-transitive implies Tarski-Class X is epsilon-transitive
  proof
   consider A such that
A1:  Tarski-Class(X,A) = Tarski-Class X by Th22;
      Tarski-Class(X,A) c= Tarski-Class(X,succ A) &
     Tarski-Class(X,succ A) c= Tarski-Class X by Th18;
then A2:  Tarski-Class(X,A) = Tarski-Class(X,succ A) by A1,XBOOLE_0:def 10;
   assume X is epsilon-transitive;
   hence thesis by A1,A2,Th25;
  end;

theorem
 Th28: Y in Tarski-Class X implies Card Y <` Card Tarski-Class X
  proof assume
A1:  Y in Tarski-Class X;
      bool Y c= Tarski-Class X
     proof let x;
      assume x in bool Y;
      hence x in Tarski-Class X by A1,Th6;
     end;
    then Card Y <` Card bool Y & Card bool Y <=` Card Tarski-Class X
     by CARD_1:27,30;
   hence Card Y <` Card Tarski-Class X;
  end;

theorem
 Th29: Y in Tarski-Class X implies not Y,Tarski-Class X are_equipotent
  proof assume Y in Tarski-Class X;
    then Card Y <` Card Tarski-Class X by Th28;
    then Card Y <> Card Tarski-Class X;
   hence thesis by CARD_1:21;
  end;

theorem
 Th30: x in Tarski-Class X & y in Tarski-Class X implies
   {x} in Tarski-Class X & {x,y} in Tarski-Class X
  proof assume
A1:  x in Tarski-Class X & y in Tarski-Class X;
    then {x} c= bool x & bool x in Tarski-Class X by Th7,ZFMISC_1:80;
   hence
A2:  {x} in Tarski-Class X by Th6;
    then bool {x} = {{},{x}} & bool {x} in Tarski-Class X by Th7,ZFMISC_1:30;
then A3:  not {{},{x}},Tarski-Class X are_equipotent by Th29;
      now assume
A4:    x <> y;
        {{},{x}},{x,y} are_equipotent
       proof
         defpred C[set] means $1 = {};
         deffunc f(set) = x;
         deffunc g(set) = y;
         consider f such that
A5:       dom f = {{},{x}} & for z st z in {{},{x}} holds
          (C[z] implies f.z = f(z)) & (not C[z] implies f.z = g(z))
           from LambdaC;
        take f;
        thus f is one-to-one
          proof let x1,x2 be set; assume x1 in dom f & x2 in dom f;
            then {} <> {x} & (x1 = {} or x1 = {x}) & (x2 = {} or x2 = {x}) &
             (x1 = {} implies f.x1 = x) & (x1 <> {} implies f.x1 = y) &
              (x2 = {} implies f.x2 = x) & (x2 <> {} implies f.x2 = y)
             by A5,TARSKI:def 2;
           hence thesis by A4;
          end;
        thus dom f = {{},{x}} by A5;
        thus rng f c= {x,y}
          proof let z; assume z in rng f;
           then consider u being set such that
A6:          u in dom f & z = f.u by FUNCT_1:def 5;
              u = {} or u <> {};
            then z = x or z = y by A5,A6;
           hence thesis by TARSKI:def 2;
          end;
        let z; assume z in {x,y};
then A7:       z = x or z = y by TARSKI:def 2;
A8:       {} in dom f & {x} in dom f & {} <> {x} by A5,TARSKI:def 2;
         then f.{} = x & f.{x} = y by A5;
        hence z in rng f by A7,A8,FUNCT_1:def 5;
       end;
      then not {x,y},Tarski-Class X are_equipotent & {x,y} c= Tarski-Class X
       by A1,A3,WELLORD2:22,ZFMISC_1:38;
     hence thesis by Th8;
    end;
   hence thesis by A2,ENUMSET1:69;
  end;

theorem
 Th31: x in Tarski-Class X & y in Tarski-Class X implies [x,y] in
 Tarski-Class X
  proof assume x in Tarski-Class X & y in Tarski-Class X;
    then {x,y} in Tarski-Class X & {x} in Tarski-Class X by Th30;
    then {{x,y},{x}} in Tarski-Class X by Th30;
   hence thesis by TARSKI:def 5;
  end;

theorem
   Y c= Tarski-Class X & Z c= Tarski-Class X implies [:Y,Z:] c= Tarski-Class X
  proof assume
A1:  Y c= Tarski-Class X & Z c= Tarski-Class X;
   let x; assume
A2:  x in [:Y,Z:];
then A3:  x = [x`1,x`2] by MCART_1:23;
      x`1 in Y & x`2 in Z by A2,MCART_1:10; hence x in
 Tarski-Class X by A1,A3,Th31;
  end;

definition let A;
 func Rank(A) means
:Def6:
   ex L st it = last L & dom L = succ A & L.{} = {} &
    (for C st succ C in succ A holds L.succ C = bool(L.C)) &
     for C st C in succ A & C <> {} & C is_limit_ordinal
           holds L.C = union rng(L|C);
  correctness
proof
  deffunc C(Ordinal,set) = bool $2;
  deffunc D(Ordinal,T-Sequence) = union rng $2;
  thus (ex x,L st x = last L & dom L = succ A & L.{} = {} &
     (for C st succ C in succ A holds L.succ C = C(C,L.C)) &
      for C st C in succ A & C <> {} & C is_limit_ordinal
             holds L.C = D(C,L|C) ) &
   for x1,x2 being set st
    (ex L st x1 = last L & dom L = succ A & L.{} = {} &
      (for C st succ C in succ A holds L.succ C = C(C,L.C)) &
       for C st C in succ A & C <> {} & C is_limit_ordinal
              holds L.C = D(C,L|C) ) &
    (ex L st x2 = last L & dom L = succ A & L.{} = {} &
      (for C st succ C in succ A holds L.succ C = C(C,L.C)) &
       for C st C in succ A & C <> {} & C is_limit_ordinal
              holds L.C = D(C,L|C) )
     holds x1 = x2 from TS_Def;
  end;
end;

deffunc F(Ordinal) = Rank $1;

Lm2:
 now
   deffunc C(Ordinal,set) = bool $2;
   deffunc D(Ordinal,T-Sequence) = union rng $2;
   A1:  for A,x holds x = F(A) iff
     ex L st x = last L & dom L = succ A & L.{} = {} &
      (for C st succ C in succ A holds L.succ C = C(C,L.C)) &
       for C st C in succ A & C <> {} & C is_limit_ordinal
              holds L.C = D(C,L|C) by Def6;
  thus F({}) = {} from TS_Result0(A1);
  thus for A holds F(succ A) = C(A,F(A)) from TS_ResultS(A1);
  thus A <> {} & A is_limit_ordinal & dom L = A &
     (for B st B in A holds L.B = Rank B) implies Rank A = union rng L
    proof assume that
A2:    A <> {} & A is_limit_ordinal and
A3:    dom L = A and
A4:    for B st B in A holds L.B = F(B);
     thus F(A) = D(A,L) from TS_ResultL(A1,A2,A3,A4);
    end;
 end;

theorem
   Rank {} = {} by Lm2;

theorem
   Rank succ A = bool Rank A by Lm2;

theorem
 Th35: A <> {} & A is_limit_ordinal implies
   for x holds x in Rank A iff ex B st B in A & x in Rank B
  proof assume
A1:  A <> {} & A is_limit_ordinal;
   consider L such that
A2:  dom L = A & for B st B in A holds L.B = F(B) from TS_Lambda;
A3:  Rank A = union rng L by A1,A2,Lm2;
   let x;
   thus x in Rank A implies ex B st B in A & x in Rank B
     proof assume x in Rank A;
      then consider Y such that
A4:     x in Y & Y in rng L by A3,TARSKI:def 4;
      consider y such that
A5:     y in dom L & Y = L.y by A4,FUNCT_1:def 5;
      reconsider y as Ordinal by A5,ORDINAL1:23;
      take y;
      thus thesis by A2,A4,A5;
     end;
   given B such that
A6:  B in A & x in Rank B;
      L.B = Rank B by A2,A6;
    then Rank B in rng L by A2,A6,FUNCT_1:def 5;
   hence x in Rank A by A3,A6,TARSKI:def 4;
  end;

theorem
 Th36: X c= Rank A iff X in Rank succ A
  proof
   thus X c= Rank A implies X in Rank succ A
     proof assume X c= Rank A;
       then X in bool Rank A;
      hence thesis by Lm2;
     end;
   assume X in Rank succ A;
    then X in bool Rank A by Lm2;
   hence X c= Rank A;
  end;

theorem
 Th37: Rank A is epsilon-transitive
  proof
   defpred P[Ordinal] means X in Rank $1 implies X c= Rank $1;
A1:for A st for B st B in A holds P[B] holds P[A]
     proof let A such that
A2:     for B st B in A holds P[B];
      let X such that
A3:     X in Rank A;
      let x such that
A4:     x in X;
A5:     now assume
A6:      A is_limit_ordinal;
        then consider B such that
A7:      B in A & X in Rank B by A3,Lm2,Th35;
           X c= Rank B by A2,A7; hence x in Rank A by A4,A6,A7,Th35;
       end;
         now assume not A is_limit_ordinal;
        then consider B such that
A8:      A = succ B by ORDINAL1:42;
           B in A & X c= Rank B by A3,A8,Th36,ORDINAL1:10;
         then x c= Rank B by A2,A4;
        hence x in Rank A by A8,Th36;
       end;
      hence thesis by A5;
     end;
      for A holds P[A] from Transfinite_Ind(A1);
   hence P[A];
  end;

theorem
 Th38: X in Rank A implies X c= Rank A
  proof
      Rank A is epsilon-transitive by Th37;
   hence thesis by ORDINAL1:def 2;
  end;

theorem
    Rank A c= Rank succ A
  proof
      Rank A in bool Rank A by ZFMISC_1:def 1;
    then Rank A in Rank succ A by Lm2;
   hence thesis by Th38;
  end;

theorem
 Th40: union Rank A c= Rank A
  proof let x; assume
      x in union Rank A;
   then consider X such that
A1:  x in X & X in Rank A by TARSKI:def 4;
      X c= Rank A by A1,Th38;
   hence x in Rank A by A1;
  end;

theorem
    X in Rank A implies union X in Rank A
  proof assume
A1:  X in Rank A;
A2:  now given B such that
A3:   A = succ B;
        X c= Rank B by A1,A3,Th36;
      then union X c= union Rank B & union Rank B c= Rank B by Th40,ZFMISC_1:95
;
      then union X c= Rank B by XBOOLE_1:1;
     hence thesis by A3,Th36;
    end;
      now assume
A4:   A <> {} & for B holds A <> succ B;
then A5:   A is_limit_ordinal by ORDINAL1:42;
     then consider B such that
A6:   B in A & X in Rank B by A1,A4,Th35;
        X c= Rank B by A6,Th38;
      then union X c= union Rank B & union Rank B c= Rank B by Th40,ZFMISC_1:95
;
then A7:    union X c= Rank B & succ B c= A & succ B <> A
        by A4,A6,ORDINAL1:33,XBOOLE_1:1;
      then succ B c< A by XBOOLE_0:def 8;
      then union X in Rank succ B & succ B in A by A7,Th36,ORDINAL1:21;
     hence thesis by A5,Th35;
    end;
   hence union X in Rank A by A1,A2,Lm2;
  end;

theorem
 Th42: A in B iff Rank A in Rank B
  proof
   defpred OnP[Ordinal,Ordinal] means $1 in $2 implies Rank $1 in Rank $2;
A1:  now let A;
defpred P[Ordinal] means OnP[A,$1];
A2:  for B st for C st C in B holds P[C] holds P[B]
       proof let B such that
A3:       for C st C in B holds OnP[A,C] and
A4:       A in B;
A5:       now given C such that
A6:        B = succ C;
             C in B by A6,ORDINAL1:10;
then A7:        A in C implies Rank A in Rank C by A3;
             now assume A8: not A in C;
              A c= C & A <> C iff A c< C by XBOOLE_0:def 8;
            hence Rank A = Rank C by A4,A6,A8,ORDINAL1:21,34;
           end;
           then Rank A c= Rank C by A7,Th38;
          hence thesis by A6,Th36;
         end;
           now assume for C holds B <> succ C;
then A9:        B is_limit_ordinal & B <> succ A by ORDINAL1:42;
           succ A c= B & Rank A c= Rank A by A4,ORDINAL1:33;
           then succ A c< B by A9,XBOOLE_0:def 8;
           then succ A in B & Rank A in Rank succ A by Th36,ORDINAL1:21;
          hence thesis by A9,Th35;
         end;
        hence thesis by A5;
       end;
     thus for B holds P[B] from Transfinite_Ind(A2);
    end;
   hence OnP[A,B];
   assume
A10:  Rank A in Rank B & not A in B;
    then B in A or B = A by ORDINAL1:24;
   hence contradiction by A1,A10;
  end;

theorem
 Th43: A c= B iff Rank A c= Rank B
  proof
   thus A c= B implies Rank A c= Rank B
     proof A1: A c< B iff A c= B & A <> B by XBOOLE_0:def 8;
       assume A c= B;
       then A = B or A in B by A1,ORDINAL1:21;
       then Rank A = Rank B or Rank A in Rank B by Th42;
      hence thesis by Th38;
     end;
   assume
A2:  Rank A c= Rank B & not A c= B;
    then B in A by ORDINAL1:26;
    then Rank B in Rank A by Th42;
   hence contradiction by A2,ORDINAL1:7;
  end;

theorem
 Th44: A c= Rank A
  proof
  defpred P[Ordinal] means $1 c= Rank $1;
A1: P[{}] by XBOOLE_1:2;
A2:  P[B] implies P[succ B]
     proof assume B c= Rank B;
       then B in Rank succ B by Th36;
       then B c= Rank succ B & {B} c= Rank succ B by Th38,ZFMISC_1:37;
       then B \/ {B} c= Rank succ B by XBOOLE_1:8;
      hence thesis by ORDINAL1:def 1;
     end;
A3:  for A st A <> {} & A is_limit_ordinal & for B st B in A holds P[B]
       holds P[A]
     proof let A such that
A4:    A <> {} & A is_limit_ordinal and
A5:    for B st B in A holds B c= Rank B;
      let x; assume
A6:    x in A;
      then reconsider B = x as Ordinal by ORDINAL1:23;
         succ B in A by A4,A6,ORDINAL1:41;
       then B c= Rank B & succ B c= A by A5,A6,ORDINAL1:def 2;
       then B in Rank succ B & Rank succ B c= Rank A by Th36,Th43;
      hence thesis;
     end;
     for B holds P[B] from Ordinal_Ind(A1,A2,A3);
   hence thesis;
  end;

theorem
    for A,X st X in Rank A holds
  not X,Rank A are_equipotent & Card X <` Card Rank A
  proof
   defpred OnP[Ordinal] means
    for X st X in Rank $1 holds not X,Rank $1 are_equipotent;
A1:for A st for B st B in A holds OnP[B] holds OnP[A]
     proof let A such that
A2:     for B st B in A holds OnP[B];
      let X; assume
A3:     X in Rank A;
A4:     now given B such that
A5:      A = succ B;
           B in A by A5,ORDINAL1:10;
         then B c= A & Rank succ B = bool Rank B by Lm2,ORDINAL1:def 2;
         then X c= Rank B & not Rank B,Rank A are_equipotent & Rank B c= Rank
A
          by A3,A5,Th43,CARD_1:29;
        hence thesis by CARD_1:44;
       end;
         now assume
A6:      A <> {} & for B holds A <> succ B;
         then A is_limit_ordinal by ORDINAL1:42;
        then consider B such that
A7:      B in A & X in Rank B by A3,A6,Th35;
A8:      not X,Rank B are_equipotent by A2,A7;
           Rank B in Rank A by A7,Th42;
         then X c= Rank B & Rank B c= Rank A by A7,Th38;
        hence thesis by A8,CARD_1:44;
       end;
      hence thesis by A3,A4,Lm2;
     end;
A9:  for A holds OnP[A] from Transfinite_Ind(A1);
   let A,X; assume A10: X in Rank A;
  then X c= Rank A & not X,Rank A are_equipotent by A9,Th38;
    then Card X <=` Card Rank A & Card X <> Card Rank A by CARD_1:21,27;
   hence thesis by A9,A10,CARD_1:13;
  end;

theorem
    X c= Rank A iff bool X c= Rank succ A
  proof
   thus X c= Rank A implies bool X c= Rank succ A
     proof assume
A1:     X c= Rank A;
      let x;
      assume x in bool X;
       then x c= Rank A & Rank succ A = bool Rank A by A1,Lm2,XBOOLE_1:1;
      hence thesis;
     end;
   assume
A2:  bool X c= Rank succ A;
   let x; assume x in X;
    then { x } c= X by ZFMISC_1:37;
    then { x } in bool X & Rank succ A = bool Rank A by Lm2;
    then { x } c= Rank A & x in { x } by A2,TARSKI:def 1;
   hence x in Rank A;
  end;

theorem
 Th47: X c= Y & Y in Rank A implies X in Rank A
  proof assume
A1:  X c= Y & Y in Rank A;
A2:  now given B such that
A3:   A = succ B;
A4:   Rank succ B = bool Rank B by Lm2;
      then X c= Rank B by A1,A3,XBOOLE_1:1;
     hence X in Rank A by A3,A4;
    end;
      now assume for B holds A <> succ B;
then A5:   A is_limit_ordinal by ORDINAL1:42;
     then consider B such that
A6:   B in A & Y in Rank B by A1,Lm2,Th35;
        Y c= Rank B by A6,Th38;
      then X c= Rank B by A1,XBOOLE_1:1;
      then X in bool Rank B & bool Rank B = Rank succ B & succ B in A
       by A5,A6,Lm2,ORDINAL1:41;
     hence X in Rank A by A5,Th35;
    end;
   hence thesis by A2;
  end;

theorem
 Th48: X in Rank A iff bool X in Rank succ A
  proof
   thus X in Rank A implies bool X in Rank succ A
     proof assume A1: X in Rank A;
         bool X c= Rank A
        proof let x;
         assume x in bool X;
         hence x in Rank A by A1,Th47;
        end;
      hence thesis by Th36;
     end;
   assume bool X in Rank succ A;
    then X in bool X & bool X c= Rank A by Th36,ZFMISC_1:def 1;
   hence thesis;
  end;

theorem
 Th49: x in Rank A iff {x} in Rank succ A
  proof
      (x in Rank A iff {x} c= Rank A) &
    ({x} c= Rank A iff {x} in Rank succ A) by Th36,ZFMISC_1:37;
   hence thesis;
  end;

theorem
 Th50: x in Rank A & y in Rank A iff {x,y} in Rank succ A
  proof
      (x in Rank A & y in Rank A iff {x,y} c= Rank A) &
    ({x,y} c= Rank A iff {x,y} in Rank succ A) by Th36,ZFMISC_1:38;
   hence thesis;
  end;

theorem
   x in Rank A & y in Rank A iff [x,y] in Rank succ succ A
  proof
      (x in Rank A iff {x} in Rank succ A) &
    (x in Rank A & y in Rank A iff {x,y} in Rank succ A) &
    ({x} in Rank succ A & {x,y} in Rank succ A iff
     {{x,y},{x}} in Rank succ succ A) & {{x,y},{x}} = [x,y]
      by Th49,Th50,TARSKI:def 5;
   hence thesis;
  end;

theorem
 Th52: X is epsilon-transitive &
  Rank A /\ Tarski-Class X = Rank succ A /\ Tarski-Class X implies
   Tarski-Class X c= Rank A
  proof assume that
A1:  X is epsilon-transitive and
A2:  Rank A /\ Tarski-Class X = Rank succ A /\ Tarski-Class X;
   given x such that
A3:  x in Tarski-Class X & not x in Rank A;
      x in (Tarski-Class X) \ Rank A by A3,XBOOLE_0:def 4;
   then consider Y such that
A4:  Y in (Tarski-Class X) \ Rank A and
A5:  not ex x st x in (Tarski-Class X) \ Rank A & x in Y by TARSKI:7;
      Tarski-Class X is epsilon-transitive & Y in Tarski-Class X
     by A1,A4,Th27,XBOOLE_0:def 4;
then A6:  Y c= Tarski-Class X by ORDINAL1:def 2;
      Y c= Rank A
     proof let x; assume x in Y;
       then not x in (Tarski-Class X) \ Rank A & x in Tarski-Class X by A5,A6;
      hence x in Rank A by XBOOLE_0:def 4;
     end;
    then Y in Rank succ A & Y in Tarski-Class X by A4,Th36,XBOOLE_0:def 4;
    then Y in Rank succ A /\ Tarski-Class X & not Y in
 Rank A by A4,XBOOLE_0:def 3,def 4;
   hence contradiction by A2,XBOOLE_0:def 3;
  end;

theorem
 Th53: X is epsilon-transitive implies ex A st Tarski-Class X c= Rank A
  proof assume
A1:  X is epsilon-transitive;
   assume
A2: not Tarski-Class X c= Rank A;
A3:  Rank A /\ Tarski-Class X <> Rank succ A /\ Tarski-Class X
     proof not Tarski-Class X c= Rank A by A2;
      hence thesis by A1,Th52;
     end;
     defpred P[set] means ex A st $1 in Rank A;
   consider Power being set such that
A4:  x in Power iff x in Tarski-Class X & P[x] from Separation;
   defpred P[set,set] means
    ex A st $2 = A & not $1 in Rank A & $1 in Rank succ A;
A5:  for x,y,z st P[x,y] & P[x,z] holds y = z
     proof let x,y,z;
      given A1 being Ordinal such that
A6:    y = A1 & not x in Rank A1 & x in Rank succ A1;
      given A2 being Ordinal such that
A7:    z = A2 & not x in Rank A2 & x in Rank succ A2;
      assume y <> z;
       then A1 in A2 or A2 in A1 by A6,A7,ORDINAL1:24;
then A8:    succ A1 c= A2 or succ A2 c= A1 by ORDINAL1:33;
         now assume succ A1 c= A2;
         then Rank succ A1 c= Rank A2 by Th43;
        hence contradiction by A6,A7;
       end;
       then Rank succ A2 c= Rank A1 by A8,Th43;
      hence contradiction by A6,A7;
     end;
   consider Y such that
A9:  x in Y iff ex y st y in Power & P[y,x] from Fraenkel(A5);
      now let A;
        Rank A /\ Tarski-Class X <> Rank succ A /\ Tarski-Class X by A3;
     then consider y such that
A10:    not (y in Rank A /\ Tarski-Class X iff y in
 Rank succ A /\ Tarski-Class X)
        by TARSKI:2;
        A in succ A by ORDINAL1:10;
      then A c= succ A by ORDINAL1:def 2;
      then Rank A c= Rank succ A by Th43;
      then Rank A /\ Tarski-Class X c= Rank succ A /\
 Tarski-Class X by XBOOLE_1:26;
      then y in Rank succ A & y in Tarski-Class X &
       (not y in Rank A or not y in Tarski-Class X) by A10,XBOOLE_0:def 3;
      then y in Power & P[y,A] by A4;
     hence A in Y by A9;
    end;
   hence contradiction by ORDINAL1:38;
  end;

theorem
 Th54: X is epsilon-transitive implies union X c= X
  proof assume
A1:  Y in X implies Y c= X;
   let x; assume x in union X;
   then consider Y such that
A2:  x in Y & Y in X by TARSKI:def 4;
      Y c= X by A1,A2;
   hence thesis by A2;
  end;

theorem
 Th55: X is epsilon-transitive & Y is epsilon-transitive implies
  X \/ Y is epsilon-transitive
  proof assume that
A1:  Z in X implies Z c= X and
A2:  Z in Y implies Z c= Y;
   let Z; assume Z in X \/ Y;
    then Z in X or Z in Y by XBOOLE_0:def 2;
    then (Z c= X or Z c= Y) & X c= X \/ Y & Y c= X \/ Y by A1,A2,XBOOLE_1:7;
   hence thesis by XBOOLE_1:1;
  end;

theorem
    X is epsilon-transitive & Y is epsilon-transitive implies
   X /\ Y is epsilon-transitive
  proof assume that
A1:  Z in X implies Z c= X and
A2:  Z in Y implies Z c= Y;
   let Z; assume Z in X /\ Y;
    then Z in X & Z in Y by XBOOLE_0:def 3;
    then Z c= X & Z c= Y by A1,A2;
   hence thesis by XBOOLE_1:19;
  end;

 reserve k,n for Nat;

 deffunc f(set,set) = union $2;

definition let X;
 func the_transitive-closure_of X -> set means
:Def7:
  x in it iff ex f,n st x in f.n & dom f = NAT & f.0 = X &
   for k holds f.(k+1) = union(f.k);
  existence
   proof
     consider f such that
A1:   dom f = NAT & f.0 = X &
     for n being Element of NAT holds f.(n+1) = f(n,f.n) from LambdaRecEx;
    take UNI = union rng f;
    let x;
    thus x in UNI implies
      ex f,n st x in f.n & dom f = NAT & f.0 = X &
       for k holds f.(k+1) = union(f.k)
      proof assume x in UNI;
       then consider Y such that
A2:      x in Y & Y in rng f by TARSKI:def 4;
       consider y such that
A3:      y in dom f & Y = f.y by A2,FUNCT_1:def 5;
       reconsider y as Element of NAT by A1,A3;
       take f,y; thus thesis by A1,A2,A3;
      end;
    deffunc f(set,set) = union $2;
    given g,n such that
A4:   x in g.n and
A5:   dom g = NAT & g.0 = X &
     for k holds g.(k+1) = f(k,g.k);
A6:   dom f = NAT & f.0 = X &
     for n holds f.(n+1) = f(n,f.n) by A1;
     g = f from LambdaRecUn(A5,A6);
     then g.n in rng f by A1,FUNCT_1:def 5;
    hence x in UNI by A4,TARSKI:def 4;
   end;
  uniqueness
   proof
     defpred P[set] means
     ex f,n st $1 in f.n & dom f = NAT & f.0 = X &
      for k holds f.(k+1) = union(f.k);
     let U1,U2 be set such that
A7:  x in U1 iff P[x] and
A8:  x in U2 iff P[x];
    thus U1 = U2 from Extensionality(A7,A8);
   end;
end;

canceled;

theorem
 Th58: the_transitive-closure_of X is epsilon-transitive
  proof let Y; assume Y in the_transitive-closure_of X;
   then consider f,n such that
A1:  Y in f.n and
A2:  dom f = NAT & f.0 = X &
     for k holds f.(k+1) = union(f.k) by Def7;
A3:  f.(n+1) = union(f.n) by A2;
   let x; assume x in Y;
    then x in union(f.n) by A1,TARSKI:def 4;
   hence x in the_transitive-closure_of X by A2,A3,Def7;
  end;

theorem
 Th59: X c= the_transitive-closure_of X
  proof let x such that
A1:  x in X;
   ex f st dom f = NAT & f.0 = X &
     for n being Element of NAT holds f.(n+1) = f(n,f.n)
     from LambdaRecEx;
   hence x in the_transitive-closure_of X by A1,Def7;
  end;

theorem
 Th60: X c= Y & Y is epsilon-transitive implies
  the_transitive-closure_of X c= Y
  proof assume
A1:  X c= Y & Y is epsilon-transitive;
   let x; assume x in the_transitive-closure_of X;
   then consider f,n such that
A2:  x in f.n & dom f = NAT & f.0 = X &
     for k holds f.(k+1) = union(f.k) by Def7;
     defpred P[Nat] means f.$1 c= Y;
A3:  P[0] by A1,A2;
A4:  for k st P[k] holds P[k+1]
     proof let k; assume f.k c= Y;
       then union (f.k) c= union Y & f.(k+1) = union (f.k) & f.(k+1) = f.(k+1)
&
        union Y c= Y by A1,A2,Th54,ZFMISC_1:95;
      hence thesis by XBOOLE_1:1;
     end;
     P[k] from Ind(A3,A4);
    then f.n = f.n & f.n c= Y;
   hence x in Y by A2;
  end;

theorem
 Th61: (for Z st X c= Z & Z is epsilon-transitive holds Y c= Z) & X c= Y &
   Y is epsilon-transitive implies the_transitive-closure_of X = Y
  proof assume
A1:  (for Z st X c= Z & Z is epsilon-transitive holds Y c= Z);
   assume X c= Y & Y is epsilon-transitive;
   hence the_transitive-closure_of X c= Y by Th60;
      the_transitive-closure_of X is epsilon-transitive &
     X c= the_transitive-closure_of X by Th58,Th59;
   hence Y c= the_transitive-closure_of X by A1;
  end;

theorem
 Th62: X is epsilon-transitive implies the_transitive-closure_of X = X
  proof
      (for Z st X c= Z & Z is epsilon-transitive holds X c= Z) & X c= X;
   hence thesis by Th61;
  end;

theorem
   the_transitive-closure_of {} = {} by Th62;

theorem
   the_transitive-closure_of A = A by Th62;

theorem Th65:
 X c= Y implies the_transitive-closure_of X c= the_transitive-closure_of Y
  proof assume
A1:  X c= Y;
      Y c= the_transitive-closure_of Y by Th59;
    then X c= the_transitive-closure_of Y &
     the_transitive-closure_of Y is epsilon-transitive by A1,Th58,XBOOLE_1:1;
   hence thesis by Th60;
  end;

theorem
   the_transitive-closure_of the_transitive-closure_of X =
   the_transitive-closure_of X
  proof
      the_transitive-closure_of X is epsilon-transitive by Th58;
   hence thesis by Th62;
  end;

theorem
   the_transitive-closure_of (X \/ Y) =
   the_transitive-closure_of X \/ the_transitive-closure_of Y
  proof
      X c= the_transitive-closure_of X & Y c= the_transitive-closure_of Y
     by Th59;
    then X \/ Y c= the_transitive-closure_of X \/ the_transitive-closure_of Y
&
     the_transitive-closure_of X is epsilon-transitive &
      the_transitive-closure_of Y is epsilon-transitive by Th58,XBOOLE_1:13
;
    then the_transitive-closure_of (X \/ Y) c=
     the_transitive-closure_of
      (the_transitive-closure_of X \/ the_transitive-closure_of Y) &
      the_transitive-closure_of X \/ the_transitive-closure_of Y
       is epsilon-transitive by Th55,Th65;
   hence the_transitive-closure_of (X \/ Y) c=
      the_transitive-closure_of X \/ the_transitive-closure_of Y by Th62;
      X c= X \/ Y & Y c= X \/ Y by XBOOLE_1:7;
    then the_transitive-closure_of X c= the_transitive-closure_of (X \/ Y) &
     the_transitive-closure_of Y c= the_transitive-closure_of (X \/ Y) by Th65;
   hence thesis by XBOOLE_1:8;
  end;

theorem
   the_transitive-closure_of (X /\ Y) c=
   the_transitive-closure_of X /\ the_transitive-closure_of Y
  proof
      X /\ Y c= X & X /\ Y c= Y by XBOOLE_1:17;
    then the_transitive-closure_of (X /\ Y) c= the_transitive-closure_of X &
     the_transitive-closure_of (X /\ Y) c= the_transitive-closure_of Y by Th65;
   hence thesis by XBOOLE_1:19;
  end;

theorem
 Th69: ex A st X c= Rank A
  proof the_transitive-closure_of X is epsilon-transitive by Th58;
   then consider A such that
A1:  Tarski-Class the_transitive-closure_of X c= Rank A by Th53;
   take A;
      the_transitive-closure_of X in Tarski-Class the_transitive-closure_of X &
     X c= the_transitive-closure_of X by Th5,Th59;
    then X in Tarski-Class the_transitive-closure_of X by Th6;
    then X in Rank A & Rank A is epsilon-transitive by A1,Th37;
   hence thesis by ORDINAL1:def 2;
  end;

definition let X;
 func the_rank_of X -> Ordinal means
:Def8:   X c= Rank it & for B st X c= Rank B holds it c= B;
  existence
   proof
      defpred P[Ordinal] means X c= Rank $1;
A1:   ex A st P[A] by Th69;
    thus ex A st P[A] & for B st P[B] holds A c= B from Ordinal_Min(A1);
   end;
  uniqueness
   proof let A1,A2 be Ordinal such that
A2:  X c= Rank A1 & for B st X c= Rank B holds A1 c= B and
A3:  X c= Rank A2 & for B st X c= Rank B holds A2 c= B;
    thus A1 c= A2 & A2 c= A1 by A2,A3;
   end;
end;

canceled;

theorem
 Th71: the_rank_of bool X = succ the_rank_of X
  proof
A1:  X c= Rank the_rank_of X &
     for A st X c= Rank A holds the_rank_of X c= A by Def8;
A2:  bool X c= Rank succ the_rank_of X
     proof let x;
      assume x in bool X;
       then x c= Rank the_rank_of X &
        bool Rank the_rank_of X = Rank succ the_rank_of X by A1,Lm2,XBOOLE_1:1;
      hence thesis;
     end;
      for A st bool X c= Rank A holds succ the_rank_of X c= A
     proof let A such that
A3:     bool X c= Rank A;
  defpred P[Ordinal] means X in Rank $1;
       A4: X in bool X by ZFMISC_1:def 1;
then A5:     ex A st P[A] by A3;
      consider B such that
A6:     P[B] & for C st P[C] holds B c= C from Ordinal_Min(A5);
         now assume for C holds B <> succ C;
         then B is_limit_ordinal by ORDINAL1:42;
        then consider C such that
A7:       C in B & X in Rank C by A6,Lm2,Th35;
           B c= C by A6,A7;
        hence contradiction by A7,ORDINAL1:7;
       end;
      then consider C such that
A8:     B = succ C;
         X c= Rank C by A6,A8,Th36;
       then the_rank_of X c= C by Def8;
       then the_rank_of X in B by A8,ORDINAL1:34;
       then succ the_rank_of X c= B & B c= A by A3,A4,A6,ORDINAL1:33;
      hence thesis by XBOOLE_1:1;
     end;
   hence thesis by A2,Def8;
  end;

theorem
   the_rank_of Rank A = A
  proof
      Rank A c= Rank A & for B st Rank A c= Rank B holds A c= B by Th43;
   hence thesis by Def8;
  end;

theorem
 Th73: X c= Rank A iff the_rank_of X c= A
  proof
   thus X c= Rank A implies the_rank_of X c= A by Def8;
   assume the_rank_of X c= A;
    then Rank the_rank_of X c= Rank A & X c= Rank the_rank_of X by Def8,Th43;
   hence thesis by XBOOLE_1:1;
  end;

theorem
 Th74: X in Rank A iff the_rank_of X in A
  proof
   thus X in Rank A implies the_rank_of X in A
     proof assume
       X in Rank A;
       then bool X in Rank succ A by Th48;
       then bool X c= Rank A & the_rank_of bool X = succ the_rank_of X
        by Th36,Th71;
       then the_rank_of X in the_rank_of bool X & the_rank_of bool X c= A
        by Def8,ORDINAL1:10;
      hence thesis;
     end;
   assume the_rank_of X in A;
    then succ the_rank_of X c= A & X c= Rank the_rank_of X by Def8,ORDINAL1:33
;
    then X in Rank succ the_rank_of X & Rank succ the_rank_of X c= Rank A by
Th36,Th43;
   hence thesis;
  end;

theorem
   X c= Y implies the_rank_of X c= the_rank_of Y
  proof assume
A1:  X c= Y;
      Y c= Rank the_rank_of Y by Def8;
    then X c= Rank the_rank_of Y by A1,XBOOLE_1:1;
   hence thesis by Def8;
  end;

theorem
 Th76: X in Y implies the_rank_of X in the_rank_of Y
  proof assume
A1:  X in Y;
      Y c= Rank the_rank_of Y by Def8; hence thesis by A1,Th74;
  end;

theorem
 Th77: the_rank_of X c= A iff for Y st Y in X holds the_rank_of Y in A
  proof
   set R = the_rank_of X;
A1:  X c= Rank R & for B st X c= Rank B holds R c= B by Def8;
   thus the_rank_of X c= A implies for Y st Y in X holds the_rank_of Y in A
     proof assume
A2:     the_rank_of X c= A;
      let Y; assume Y in X;
       then Y in Rank R & Rank R c= Rank A by A1,A2,Th43;
      hence the_rank_of Y in A by Th74;
     end;
   assume
A3:  for Y st Y in X holds the_rank_of Y in A;
      X c= Rank A
     proof let x;
      assume x in X;
       then the_rank_of x in A by A3;
      hence x in Rank A by Th74;
     end;
   hence thesis by Def8;
  end;

theorem
 Th78: A c= the_rank_of X iff for B st B in A ex Y st Y in
 X & B c= the_rank_of Y
  proof
   thus A c= the_rank_of X implies
      for B st B in A ex Y st Y in X & B c= the_rank_of Y
     proof assume
A1:     A c= the_rank_of X;
      let B; assume B in A;
       then not the_rank_of X c= B by A1,ORDINAL1:7;
       then not X c= Rank B by Def8;
then A2:     X \ Rank B <> {} by XBOOLE_1:37;
      consider x being Element of X \ Rank B;
      take x;
A3:     x in X & not x in Rank B by A2,XBOOLE_0:def 4;
      thus x in X by A2,XBOOLE_0:def 4;
         not the_rank_of x in B by A3,Th74;
      hence thesis by ORDINAL1:26;
     end;
   assume
A4:  for B st B in A ex Y st Y in X & B c= the_rank_of Y;
   let x; assume
A5:  x in A;
   then reconsider x as Ordinal by ORDINAL1:23;
   consider Y such that
A6:  Y in X & x c= the_rank_of Y by A4,A5;
      the_rank_of Y in the_rank_of X by A6,Th76;
   hence thesis by A6,ORDINAL1:22;
  end;

theorem
   the_rank_of X = {} iff X = {}
  proof
   thus the_rank_of X = {} implies X = {}
     proof assume the_rank_of X = {};
       then X c= Rank {} & Rank {} = {} by Def8,Lm2;
      hence X = {} by XBOOLE_1:3;
     end;
   assume
    X = {};
    then for Y st Y in X holds the_rank_of Y in {};
   hence the_rank_of X c= {} by Th77;
   thus {} c= the_rank_of X by XBOOLE_1:2;
  end;

theorem
 Th80: the_rank_of X = succ A implies ex Y st Y in X & the_rank_of Y = A
  proof assume
A1:  the_rank_of X = succ A;
    then A in succ A & succ A c= the_rank_of X by ORDINAL1:10;
   then consider Y such that
A2:  Y in X & A c= the_rank_of Y by Th78;
   take Y;
      the_rank_of Y in the_rank_of X by A2,Th76;
    then the_rank_of Y c= A by A1,ORDINAL1:34;
   hence thesis by A2,XBOOLE_0:def 10;
  end;

theorem
   the_rank_of A = A
  proof A c= Rank A by Th44;
   hence the_rank_of A c= A by Th73;
     defpred P[Ordinal] means $1 c= the_rank_of $1;
A1:  for A st for B st B in A holds P[B] holds P[A]
     proof let A such that
A2:     for B st B in A holds B c= the_rank_of B;
         now let B such that
A3:       B in A;
        reconsider Y = B as set;
        take Y; thus Y in A & B c= the_rank_of Y by A2,A3;
       end;
      hence thesis by Th78;
     end;
     P[B] from Transfinite_Ind(A1);
   hence thesis;
  end;

theorem
    the_rank_of Tarski-Class X <> {} &
   the_rank_of Tarski-Class X is_limit_ordinal
  proof
A1:  Tarski-Class X c= Rank the_rank_of Tarski-Class X &
     for A st Tarski-Class X c= Rank A holds the_rank_of Tarski-Class X c= A
      by Def8;
   thus the_rank_of Tarski-Class X <> {}
     proof assume the_rank_of Tarski-Class X = {};
       then Tarski-Class X c= {} by Def8,Lm2;
      hence contradiction by XBOOLE_1:3;
     end;
   assume not thesis;
   then consider A such that
A2:  the_rank_of Tarski-Class X = succ A by ORDINAL1:42;
   consider Y such that
A3:  Y in Tarski-Class X & the_rank_of Y = A by A2,Th80;
A4:    bool Y in Tarski-Class X & the_rank_of bool Y = succ A
     by A3,Th7,Th71;
    then bool Y c= Rank A by A1,A2,Th36;
    then succ A c= A by A4,Def8;
    then A in A by ORDINAL1:33;
   hence contradiction;
  end;

Back to top