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 = the Element of X;
assume A1: 1 < card X ; :: thesis: ex x1, x2 being set st
( x1 in X & x2 in X & x1 <> x2 )
then X <> {} ;
then A2: the Element of X in X ;
now :: thesis: ex x2 being set st
( x2 in X & not x2 = the Element of X )
assume A3: for x2 being set st x2 in X holds
x2 = the Element of X ; :: thesis: contradiction
now :: thesis: for x being object holds
( ( x in X implies x in { the Element of X} ) & ( x in { the Element of X} implies x in X ) )
let x be object ; :: thesis: ( ( x in X implies x in { the Element of X} ) & ( x in { the Element of X} implies x in X ) )
hereby :: thesis: ( x in { the Element of X} implies x in X )
assume x in X ; :: thesis: x in { the Element of X}
then x = the Element of X by A3;
hence x in { the Element of X} by TARSKI:def 1; :: thesis: verum
end;
assume x in { the Element of X} ; :: thesis: x in X
hence x in X by A2, TARSKI:def 1; :: thesis: verum
end;
then X = { the Element of X} by TARSKI:2;
hence contradiction by A1, CARD_1:30; :: thesis: verum
end;
hence ex x1, x2 being set st
( x1 in X & x2 in X & x1 <> x2 ) ; :: thesis: verum