let A, B be Ordinal; :: thesis: ( A is_cofinal_with B & B is_cofinal_with A implies A = B )
assume ( A is_cofinal_with B & B is_cofinal_with A ) ; :: thesis: A = B
hence ( A c= B & B c= A ) by Th22; :: according to XBOOLE_0:def 10 :: thesis: verum