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 A1: ( x in Tarski-Class X & y in Tarski-Class X ) ; :: thesis: ( {x} in Tarski-Class X & {x,y} in Tarski-Class X )
then ( {x} c= bool x & bool x in Tarski-Class X ) by Th7, ZFMISC_1:80;
hence A2: {x} in Tarski-Class X by Th6; :: thesis: {x,y} in Tarski-Class X
then ( bool {x} = {{} ,{x}} & bool {x} in Tarski-Class X ) by Th7, ZFMISC_1:30;
then A3: not {{} ,{x}}, Tarski-Class X are_equipotent by Th29;

now

assume A4: 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
A5: ( 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 & dom f = {{} ,{x}} & rng f = {x,y} )
thus f is one-to-one :: thesis: ( dom f = {{} ,{x}} & rng f = {x,y} )

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )
then ( {} <> {x} & ( x1 = {} or x1 = {x} ) & ( x2 = {} or x2 = {x} ) & ( x1 = {} implies f . x1 = x ) & ( x1 <> {} implies f . x1 = y ) & ( x2 = {} implies f . x2 = x ) & ( x2 <> {} implies f . x2 = y ) ) by A5, TARSKI:def 2;
hence ( not f . x1 = f . x2 or x1 = x2 ) by A4; :: thesis: verum

end;

thus dom f = {{} ,{x}} by A5; :: thesis: rng f = {x,y}
thus rng f c= {x,y} :: according to XBOOLE_0:def 10 :: thesis: {x,y} c= rng 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 A5;
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 rng f )
assume z in {x,y} ; :: thesis: z in rng f
then A6: ( z = x or z = y ) by TARSKI:def 2;
A7: ( {} in dom f & {x} in dom f & {} <> {x} ) by A5, TARSKI:def 2;
then ( f . {} = x & f . {x} = y ) by A5;
hence z in rng f by A6, A7, FUNCT_1:def 5; :: thesis: verum

end;

then ( not {x,y}, Tarski-Class X are_equipotent & {x,y} c= Tarski-Class X ) by A1, A3, WELLORD2:22, ZFMISC_1:38;
hence {x,y} in Tarski-Class X by Th8; :: thesis: verum

end;

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