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 )
assume A1: for x, y being set st x in D & y in D holds
x = y ; :: thesis: card D = 1
consider x being Element of D;
for y being set holds
( y in D iff y = x ) by A1;
then D = {x} by TARSKI:def 1;
hence card D = 1 by CARD_2:60; :: thesis: verum