:: deftheorem Def1 defines cf CARD_5:def 1 :
for M, b₂ being Cardinal holds
( b₂ = cf M iff ( M is_cofinal_with b₂ & ( for N being Cardinal st M is_cofinal_with N holds
b₂ c= N ) ) );