let X be set ; :: thesis: for A being Ordinal st Tarski-Class X,A = Tarski-Class X,(succ A) holds
Tarski-Class X,A = Tarski-Class X
let A be Ordinal; :: thesis: ( Tarski-Class X,A = Tarski-Class X,(succ A) implies Tarski-Class X,A = Tarski-Class X )
assume A1: Tarski-Class X,A = Tarski-Class X,(succ A) ; :: thesis: Tarski-Class X,A = Tarski-Class X
A2: {} c= A ;
A3: Tarski-Class X,{} c= Tarski-Class X,A by A2, Th19;
A4: ( Tarski-Class X,{} = {X} & X in {X} ) by Lm1, TARSKI:def 1;
A5: Tarski-Class X,A is_Tarski-Class_of X

proof

thus X in Tarski-Class X,A by A3, A4; :: according to CLASSES1:def 3 :: thesis: Tarski-Class X,A is Tarski
A6: Tarski-Class X,(succ A) = ({ u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class X,A & u c= v ) } \/ { (bool v) where v is Element of Tarski-Class X : v in Tarski-Class X,A } ) \/ ((bool (Tarski-Class X,A)) /\ (Tarski-Class X)) by Lm1;
A7: Tarski-Class X is_Tarski-Class_of X by Def4;
A8: Tarski-Class X is Tarski by A7, Def3;
thus for Z, Y being set st Z in Tarski-Class X,A & Y c= Z holds
Y in Tarski-Class X,A :: according to CLASSES1:def 1,CLASSES1:def 2 :: thesis: ( ( for X being set st X in Tarski-Class X,A holds
bool X in Tarski-Class X,A ) & ( for X being set holds
( not X c= Tarski-Class X,A or X, Tarski-Class X,A are_equipotent or X in Tarski-Class X,A ) ) )

proof

let Z, Y be set ; :: thesis: ( Z in Tarski-Class X,A & Y c= Z implies Y in Tarski-Class X,A )
assume A9: ( Z in Tarski-Class X,A & Y c= Z ) ; :: thesis: Y in Tarski-Class X,A
A10: Tarski-Class X is_Tarski-Class_of X by Def4;
A11: Tarski-Class X is Tarski by A10, Def3;
A12: Tarski-Class X is subset-closed by A11, Def2;
reconsider y = Y as Element of Tarski-Class X by A9, A12, Def1;
A13: ex v being Element of Tarski-Class X st
( v in Tarski-Class X,A & y c= v ) by A9;
A14: Y in { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class X,A & u c= v ) } by A13;
A15: Y in { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class X,A & u c= v ) } \/ { (bool v) where v is Element of Tarski-Class X : v in Tarski-Class X,A } by A14, XBOOLE_0:def 3;
thus Y in Tarski-Class X,A by A1, A6, A15, XBOOLE_0:def 3; :: thesis: verum

end;

thus for Y being set st Y in Tarski-Class X,A holds
bool Y in Tarski-Class X,A :: thesis: for X being set holds
( not X c= Tarski-Class X,A or X, Tarski-Class X,A are_equipotent or X in Tarski-Class X,A )

proof

let Y be set ; :: thesis: ( Y in Tarski-Class X,A implies bool Y in Tarski-Class X,A )
assume A16: Y in Tarski-Class X,A ; :: thesis: bool Y in Tarski-Class X,A
A17: bool Y in { (bool u) where u is Element of Tarski-Class X : u in Tarski-Class X,A } by A16;
A18: bool Y in { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class X,A & u c= v ) } \/ { (bool v) where v is Element of Tarski-Class X : v in Tarski-Class X,A } by A17, XBOOLE_0:def 3;
thus bool Y in Tarski-Class X,A by A1, A6, A18, XBOOLE_0:def 3; :: thesis: verum

end;

let Y be set ; :: thesis: ( not Y c= Tarski-Class X,A or Y, Tarski-Class X,A are_equipotent or Y in Tarski-Class X,A )
assume that
A19: Y c= Tarski-Class X,A and
A20: not Y, Tarski-Class X,A are_equipotent ; :: thesis: Y in Tarski-Class X,A
A21: Y c= Tarski-Class X by A19, XBOOLE_1:1;
A22: ( Y, Tarski-Class X are_equipotent or Y in Tarski-Class X ) by A8, A21, Def2;
thus Y in Tarski-Class X,A by A1, A19, A20, A22, Th13, CARD_1:44; :: thesis: verum

end;

thus ( Tarski-Class X,A c= Tarski-Class X & Tarski-Class X c= Tarski-Class X,A ) by A5, Def4; :: according to XBOOLE_0:def 10 :: thesis: verum