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 A2: Tarski-Class (X,{}) c= Tarski-Class (X,A) by Th16;
A3: ( 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 A2, A3; :: according to CLASSES1:def 3 :: thesis: Tarski-Class (X,A) is Tarski
A4: 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 A5: Tarski-Class X is Tarski ;
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 A6: ( 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 ;
then Tarski-Class X is subset-closed ;
then reconsider y = Y as Element of Tarski-Class X by A6;
ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & y c= v ) by A6;
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, A4, 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, A4, 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
A7: Y c= Tarski-Class (X,A) and
A8: not Y, Tarski-Class (X,A) are_equipotent ; :: thesis: Y in Tarski-Class (X,A)
Y c= Tarski-Class X by A7, XBOOLE_1:1;
then ( Y, Tarski-Class X are_equipotent or Y in Tarski-Class X ) by A5;
hence Y in Tarski-Class (X,A) by A1, A7, A8, Th10, CARD_1:24; :: 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