:: deftheorem Def2 defines card CARD_1:def 2 :
for X being set
for b₂ being Cardinal holds
( b₂ = card X iff X,b₂ are_equipotent );