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 )
A3: bool x in Tarski-Class X by A1, Th7;
thus A4: {x} in Tarski-Class X by A3, Th6, ZFMISC_1:80; :: thesis: {x,y} in Tarski-Class X
A5: bool {x} = {{} ,{x}} by ZFMISC_1:30;
A6: not {{} ,{x}}, Tarski-Class X are_equipotent by A4, A5, Th7, Th29;

A7: now

assume A8: x <> y ; :: thesis: {x,y} in Tarski-Class X
A9: {{} ,{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;
A15: ( x1 <> {} implies f . x1 = y ) by A10, A11;
thus ( not f . x1 = f . x2 or x1 = x2 ) by A8, A10, A11, A12, A13, A14, A15, 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 A16: z in rng f ; :: thesis: z in {x,y}
A17: ex u being set st
( u in dom f & z = f . u ) by A16, FUNCT_1:def 5;
A18: ( z = x or z = y ) by A10, A17;
thus z in {x,y} by A18, 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 A19: z in {x,y} ; :: thesis: z in proj2 f
A20: ( z = x or z = y ) by A19, 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;
A24: f . {x} = y by A10, A22;
thus z in proj2 f by A20, A21, A22, A23, A24, FUNCT_1:def 5; :: thesis: verum

end;

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

end;

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