for A being Ordinal ex M being Cardinal st
( M c= card A & A is_cofinal_with M & ( for B being Ordinal st A is_cofinal_with B holds
M c= B ) )