let X, Y be set ; :: thesis: ( ( X c< Y or X = Y or Y c< X ) iff X,Y are_c=-comparable )
thus ( ( X c< Y or X = Y or Y c< X ) implies X,Y are_c=-comparable ) :: thesis: ( not X,Y are_c=-comparable or X c< Y or X = Y or Y c< X )

proof

assume ( X c< Y or X = Y or Y c< X ) ; :: thesis: X,Y are_c=-comparable
hence ( X c= Y or Y c= X ) by XBOOLE_0:def 8; :: according to XBOOLE_0:def 9 :: thesis: verum

end;

assume ( X c= Y or Y c= X ) ; :: according to XBOOLE_0:def 9 :: thesis: ( X c< Y or X = Y or Y c< X )
hence ( X c< Y or X = Y or Y c< X ) by XBOOLE_0:def 8; :: thesis: verum