let A, B be Ordinal; :: thesis: A,B are_c=-comparable
( A c= B or B c= A ) ;
hence A,B are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum