let x, y, W be set ; :: thesis: ( W is Tarski & x in W & y in W implies ( {x} in W & {x,y} in W ) )
defpred S₁[ object ] means $1 = {} ;
assume that
A1: W is Tarski and
A2: x in W and
A3: y in W ; :: thesis: ( {x} in W & {x,y} in W )
A4: {x} c= bool x by ZFMISC_1:68;
bool x in W by A1, A2;
hence {x} in W by A1, A4, CLASSES1:def 1; :: thesis: {x,y} in W
then A5: bool {x} in W by A1;
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();
{x,y} c= rng f

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {x,y} or z in rng f )
A7: {} in {{},{x}} by TARSKI:def 2;
A8: {x} in {{},{x}} by TARSKI:def 2;
assume z in {x,y} ; :: thesis: z in rng f
then ( z = x or z = y ) by TARSKI:def 2;
then ( f . {} = z or f . {x} = z ) by A6, A7, A8;
hence z in rng f by A6, A7, A8, FUNCT_1:def 3; :: thesis: verum

end;

then A9: card {x,y} c= card {{},{x}} by A6, CARD_1:12;
A10: {x,y} c= W by A2, A3, TARSKI:def 2;
bool {x} = {{},{x}} by ZFMISC_1:24;
then card {{},{x}} in card W by A1, A5, Th1;
then card {x,y} in card W by A9, ORDINAL1:12;
hence {x,y} in W by A1, A10, CLASSES1:1; :: thesis: verum