let X, x, y be set ; :: thesis: ( x in Tarski-Class X & y in Tarski-Class X implies ( {x} in Tarski-Class X & {x,y} in Tarski-Class X ) )
assume that
A1: x in Tarski-Class X and
A2: y in Tarski-Class X ; :: thesis: ( {x} in Tarski-Class X & {x,y} in Tarski-Class X )
bool x in Tarski-Class X by A1, Th7;
hence A4: {x} in Tarski-Class X by Th6, ZFMISC_1:80; :: thesis: {x,y} in Tarski-Class X
bool {x} = {{},{x}} by ZFMISC_1:30;
then A6: not {{},{x}}, Tarski-Class X are_equipotent by A4, Th7, Th29;

now

assume A8: x <> y ; :: thesis: {x,y} in Tarski-Class X
{{},{x}},{x,y} are_equipotent

proof

defpred S₁[ set ] means $1 = {} ;
deffunc H₁( set ) -> set = x;
deffunc H₂( set ) -> set = y;
consider f being Function such that
A10: ( dom f = {{},{x}} & ( for z being set st z in {{},{x}} holds
( ( S₁[z] implies f . z = H₁(z) ) & ( not S₁[z] implies f . z = H₂(z) ) ) ) ) from PARTFUN1:sch 1();
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = {{},{x}} & proj2 f = {x,y} )
thus f is one-to-one :: thesis: ( proj1 f = {{},{x}} & proj2 f = {x,y} )

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A11: x1 in dom f and
A12: x2 in dom f ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )
A13: ( x2 = {} or x2 = {x} ) by A10, A12, TARSKI:def 2;
A14: ( x1 = {} implies f . x1 = x ) by A10, A11;
( x1 <> {} implies f . x1 = y ) by A10, A11;
hence ( not f . x1 = f . x2 or x1 = x2 ) by A8, A10, A11, A12, A13, A14, TARSKI:def 2; :: thesis: verum

end;

thus dom f = {{},{x}} by A10; :: thesis: proj2 f = {x,y}
thus rng f c= {x,y} :: according to XBOOLE_0:def 10 :: thesis: {x,y} c= proj2 f

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in {x,y} )
assume z in rng f ; :: thesis: z in {x,y}
then ex u being set st
( u in dom f & z = f . u ) by FUNCT_1:def 5;
then ( z = x or z = y ) by A10;
hence z in {x,y} by TARSKI:def 2; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {x,y} or z in proj2 f )
assume z in {x,y} ; :: thesis: z in proj2 f
then A20: ( z = x or z = y ) by TARSKI:def 2;
A21: {} in dom f by A10, TARSKI:def 2;
A22: {x} in dom f by A10, TARSKI:def 2;
A23: f . {} = x by A10, A21;
f . {x} = y by A10, A22;
hence z in proj2 f by A20, A21, A22, A23, FUNCT_1:def 5; :: thesis: verum

end;

then A25: not {x,y}, Tarski-Class X are_equipotent by A6, WELLORD2:22;
{x,y} c= Tarski-Class X by A1, A2, ZFMISC_1:38;
hence {x,y} in Tarski-Class X by A25, Th8; :: thesis: verum

end;

hence {x,y} in Tarski-Class X by A4, ENUMSET1:69; :: thesis: verum