:: deftheorem Def17 defines predecessor CARD_FIL:def 17 :
for M being non limit_cardinal Cardinal
for b₂ being Cardinal holds
( b₂ = predecessor M iff M = nextcard b₂ );