for A, B being Ordinal st A is_cofinal_with B holds
( A is limit_ordinal iff B is limit_ordinal ) by ORDINAL4:38;