let X be set ; :: thesis: ( card X = 2 implies ex x, y being object st
( x <> y & X = {x,y} ) )
assume A1: card X = 2 ; :: thesis: ex x, y being object st
( x <> y & X = {x,y} )
then consider x being object such that
A2: x in X by CARD_1:27, XBOOLE_0:def 1;
X is finite by A1;
then reconsider Y = X as finite set ;
{x} c= X by A2, ZFMISC_1:31;
then card (X \ {x}) = (card Y) - (card {x}) by Th43
.= 2 - 1 by A1, CARD_1:30 ;
then consider y being object such that
A3: X \ {x} = {y} by Th41;
take x ; :: thesis: ex y being object 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 object ; :: 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 ) ;
end;
end;
let z be object ; :: 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