let X, x, y be set ; :: thesis: ( ( x in Tarski-Class X implies {x} in Tarski-Class X ) & ( x in Tarski-Class X & y in Tarski-Class X implies {x,y} in Tarski-Class X ) )

hereby :: thesis: ( x in Tarski-Class X & y in Tarski-Class X implies {x,y} in Tarski-Class X )

assume x in Tarski-Class X ; :: thesis: {x} in Tarski-Class X
then bool x in Tarski-Class X by Th4;
hence {x} in Tarski-Class X by Th3, ZFMISC_1:68; :: thesis: verum

end;

assume that
A1: x in Tarski-Class X and
A2: y in Tarski-Class X ; :: thesis: {x,y} in Tarski-Class X
A3: {x} in Tarski-Class X by Z1, A1;
bool {x} = {{},{x}} by ZFMISC_1:24;
then A4: not {{},{x}}, Tarski-Class X are_equipotent by A3, Th4, Th25;

now :: thesis: ( x <> y implies {x,y} in Tarski-Class X )

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

proof

defpred S₁[ object ] means $1 = {} ;
deffunc H₁( object ) -> set = x;
deffunc H₂( object ) -> set = y;
consider f being Function such that
A6: ( dom f = {{},{x}} & ( for z being object 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 object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A7: x1 in dom f and
A8: x2 in dom f ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )
A9: ( x2 = {} or x2 = {x} ) by A6, A8, TARSKI:def 2;
A10: ( x1 = {} implies f . x1 = x ) by A6, A7;
( x1 <> {} implies f . x1 = y ) by A6, A7;
hence ( not f . x1 = f . x2 or x1 = x2 ) by A5, A6, A7, A8, A9, A10, TARSKI:def 2; :: thesis: verum

end;

thus dom f = {{},{x}} by A6; :: 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 object ; :: 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 object st
( u in dom f & z = f . u ) by FUNCT_1:def 3;
then ( z = x or z = y ) by A6;
hence z in {x,y} by TARSKI:def 2; :: thesis: verum

end;

let z be object ; :: 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 A11: ( z = x or z = y ) by TARSKI:def 2;
A12: {} in dom f by A6, TARSKI:def 2;
A13: {x} in dom f by A6, TARSKI:def 2;
A14: f . {} = x by A6, A12;
f . {x} = y by A6, A13;
hence z in rng f by A11, A12, A13, A14, FUNCT_1:def 3; :: thesis: verum

end;

then A15: not {x,y}, Tarski-Class X are_equipotent by A4, WELLORD2:15;
{x,y} c= Tarski-Class X by A1, A2, ZFMISC_1:32;
hence {x,y} in Tarski-Class X by A15, Th5; :: thesis: verum

end;

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