theorem :: XBOOLE_1:104

for X, Y being set holds
( ( X c< Y or X = Y or Y c< X ) iff X,Y are_c=-comparable ) ;