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 ( ( A \/ B c= A or A \/ B c= B ) & A c= A \/ B & B c= A \/ B ) by Def1, XBOOLE_1:7;
hence ( A c= B or B c= A ) by XBOOLE_0:def 10; :: according to XBOOLE_0:def 9 :: thesis: verum