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