let U1, U2 be Universe; :: thesis: ( U1 in U2 or U1 = U2 or U2 in U1 )
( ( On U1 in On U2 or On U1 = On U2 or On U2 in On U1 ) & U1 = Rank (On U1) & U2 = Rank (On U2) ) by Th54, ORDINAL1:24;
hence ( U1 in U2 or U1 = U2 or U2 in U1 ) by CLASSES1:42; :: thesis: verum