:: deftheorem Def6 defines -element CARD_1:def 7 :
for N being object
for X being set holds
( X is N -element iff card X = N );