let U1, U2 be Universe; :: thesis: U1,U2 are_c=-comparable
A1: ( On U1 c= On U2 or On U2 c= On U1 ) ;
A2: U2 = Rank (On U2) by Th50;
U1 = Rank (On U1) by Th50;
hence ( U1 c= U2 or U2 c= U1 ) by A1, A2, CLASSES1:37; :: according to XBOOLE_0:def 9 :: thesis: verum