let X be finite set ; :: thesis: ( 1 < card X implies ex x1, x2 being set st
( x1 in X & x2 in X & x1 <> x2 ) )
set x1 = choose X;
assume A1: 1 < card X ; :: thesis: ex x1, x2 being set st
( x1 in X & x2 in X & x1 <> x2 )
then X <> {} by CARD_1:47;
then A2: choose X in X ;

now

assume A3: for x2 being set st x2 in X holds
x2 = choose X ; :: thesis: contradiction

now

let x be set ; :: thesis: ( ( x in X implies x in {(choose X)} ) & ( x in {(choose X)} implies x in X ) )

hereby :: thesis: ( x in {(choose X)} implies x in X )

assume x in X ; :: thesis: x in {(choose X)}
then x = choose X by A3;
hence x in {(choose X)} by TARSKI:def 1; :: thesis: verum

end;

assume x in {(choose X)} ; :: thesis: x in X
hence x in X by A2, TARSKI:def 1; :: thesis: verum

end;

then X = {(choose X)} by TARSKI:2;
hence contradiction by A1, CARD_1:50; :: thesis: verum

end;

hence ex x1, x2 being set st
( x1 in X & x2 in X & x1 <> x2 ) ; :: thesis: verum