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

proof

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 ) & {} in {{} ,{x}} & {x} in {{} ,{x}} & {x} <> {} ) by TARSKI:def 2;
then ( f . {} = z or f . {x} = z ) by A5;
hence z in rng f by A5, A6, FUNCT_1:def 5; :: thesis: verum

end;

then card {x,y} c= card {{} ,{x}} by A5, CARD_1:28;
then A7: card {x,y} in card W by A4, ORDINAL1:22;
{x,y} c= W

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {x,y} or z in W )
assume z in {x,y} ; :: thesis: z in W
hence z in W by A2, TARSKI:def 2; :: thesis: verum

end;

hence {x,y} in W by A1, A7, CLASSES1:2; :: thesis: verum