let X be finite set ; :: thesis: ( 2 <= card X implies ex u, v being object st
( u <> v & u in X & v in X ) )
assume A1: 2 <= card X ; :: thesis: ex u, v being object st
( u <> v & u in X & v in X )
assume A2: for u, v being object holds
( not u <> v or not u in X or not v in X ) ; :: thesis: contradiction
X <> {} by A1;
then consider z being object such that
A3: z in X by XBOOLE_0:def 1;
A4: {z} c= X by ZFMISC_1:31, A3;
now :: thesis: for x being object st x in X holds
x in {z}
let x be object ; :: thesis: ( x in X implies x in {z} )
assume x in X ; :: thesis: x in {z}
then x = z by A2, A3;
hence x in {z} by TARSKI:def 1; :: thesis: verum
end;
then X c= {z} by TARSKI:def 3;
then X = {z} by A4, XBOOLE_0:def 10;
then card X = 1 by CARD_1:30;
hence contradiction by A1; :: thesis: verum