let A, B be set ; :: thesis: ( (bool A) \/ (bool B) = bool (A \/ B) implies A,B are_c=-comparable )
assume A1: (bool A) \/ (bool B) = bool (A \/ B) ; :: thesis: A,B are_c=-comparable
A \/ B in bool (A \/ B) by Def1;
then ( A \/ B in bool A or A \/ B in bool B ) by A1, XBOOLE_0:def 3;
then A2: ( A \/ B c= A or A \/ B c= B ) by Def1;
( A c= A \/ B & B c= A \/ B ) by XBOOLE_1:7;
hence ( A c= B or B c= A ) by A2; :: according to XBOOLE_0:def 9 :: thesis: verum