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
{} c= A ;
then A3: Tarski-Class (X,{}) c= Tarski-Class (X,A) by Th19;
A4: ( Tarski-Class (X,{}) = {X} & X in {X} ) by Lm1, TARSKI:def 1;
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;
Tarski-Class X is_Tarski-Class_of X by Def4;
then A8: Tarski-Class X is Tarski by 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)
Tarski-Class X is_Tarski-Class_of X by Def4;
then Tarski-Class X is Tarski by Def3;
then Tarski-Class X is subset-closed by Def2;
then reconsider y = Y as Element of Tarski-Class X by A9, Def1;
ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & y c= v ) by A9;
then 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 ) } ;
then 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 XBOOLE_0:def 3;
hence Y in Tarski-Class (X,A) by A1, A6, 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 Y in Tarski-Class (X,A) ; :: thesis: bool Y in Tarski-Class (X,A)
then bool Y in { (bool u) where u is Element of Tarski-Class X : u in Tarski-Class (X,A) } ;
then 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 XBOOLE_0:def 3;
hence bool Y in Tarski-Class (X,A) by A1, A6, 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)
Y c= Tarski-Class X by A19, XBOOLE_1:1;
then ( Y, Tarski-Class X are_equipotent or Y in Tarski-Class X ) by A8, Def2;
hence Y in Tarski-Class (X,A) by A1, A19, A20, Th13, CARD_1:44; :: thesis: verum

end;

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