let U1, U2 be Universe; :: thesis: ( U1 \/ U2 is Universe & U1 /\ U2 is Universe )
U1,U2 are_c=-comparable by Th54;
then ( U1 c= U2 or U2 c= U1 ) ;
hence ( U1 \/ U2 is Universe & U1 /\ U2 is Universe ) by XBOOLE_1:12, XBOOLE_1:28; :: thesis: verum