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

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