let A, B be set ; ( A,B are_c=-incomparable or A c= B or B c< A )
assume that
A1:
A,B are_c=-comparable
and
A2:
not A c= B
and
A3:
not B c< A
; contradiction
( A c= B or B c= A )
by A1, XBOOLE_0:def 9;
hence
contradiction
by A2, A3, XBOOLE_0:def 8; verum