theorem :: NAT_1:59

for X being finite set st 1 < card X holds
ex x1, x2 being set st
( x1 in X & x2 in X & x1 <> x2 )