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