let X be finite set ; :: thesis: ( card X = 2 implies ex x, y being set st
( x <> y & X = {x,y} ) )
assume A1: card X = 2 ; :: thesis: ex x, y being set st
( x <> y & X = {x,y} )
then consider x being set such that
A2: x in X by CARD_1:47, XBOOLE_0:def 1;
{x} c= X by A2, ZFMISC_1:37;
then card (X \ {x}) = (card X) - (card {x}) by Th63
.= 2 - 1 by A1, CARD_1:50 ;
then consider y being set such that
A3: X \ {x} = {y} by Th60;
take x ; :: thesis: ex y being set st
( x <> y & X = {x,y} )
take y ; :: thesis: ( x <> y & X = {x,y} )
x in {x} by TARSKI:def 1;
hence x <> y by A3, XBOOLE_0:def 5; :: thesis: X = {x,y}
thus X c= {x,y} :: according to XBOOLE_0:def 10 :: thesis: {x,y} c= X

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in X or z in {x,y} )
assume A4: z in X ; :: thesis: z in {x,y}

per cases ( z = x or z <> x ) ;

suppose z = x ; :: thesis: z in {x,y}

hence z in {x,y} by TARSKI:def 2; :: thesis: verum

end;

suppose z <> x ; :: thesis: z in {x,y}

then not z in {x} by TARSKI:def 1;
then z in {y} by A3, A4, XBOOLE_0:def 5;
then z = y by TARSKI:def 1;
hence z in {x,y} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {x,y} or z in X )
assume z in {x,y} ; :: thesis: z in X
then A5: ( z = x or z = y ) by TARSKI:def 2;
y in X \ {x} by A3, TARSKI:def 1;
hence z in X by A2, A5; :: thesis: verum