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