:: deftheorem Def1 defines cardinal CARD_1:def 1 :
for IT being object holds
( IT is cardinal iff ex B being Ordinal st
( IT = B & ( for A being Ordinal st A,B are_equipotent holds
B c= A ) ) );