let D be non empty set ; :: thesis: ( ( for x, y being set st x in D & y in D holds
x = y ) implies card D = 1 )
set x = the Element of D;
assume for x, y being set st x in D & y in D holds
x = y ; :: thesis: card D = 1
then for y being object holds
( y in D iff y = the Element of D ) ;
then D = { the Element of D} by TARSKI:def 1;
hence card D = 1 by CARD_2:42; :: thesis: verum