let U1, U2 be Universe; :: thesis: ( U1 c= U2 or U2 in U1 )
A1: ( On U1 c= On U2 or On U2 in On U1 ) by ORDINAL1:26;
A2: U2 = Rank (On U2) by Th54;
U1 = Rank (On U1) by Th54;
hence ( U1 c= U2 or U2 in U1 ) by A1, A2, CLASSES1:42, CLASSES1:43; :: thesis: verum