let U1, U2, U3 be Universe; :: thesis: ( U1 in U2 & U2 in U3 implies U1 in U3 )
assume that
A1: U1 in U2 and
A2: U2 in U3 ; :: thesis: U1 in U3
A3: U3 = Rank (On U3) by Th54;
A4: U2 = Rank (On U2) by Th54;
then A5: On U2 in On U3 by A2, A3, CLASSES1:42;
A6: U1 = Rank (On U1) by Th54;
then On U1 in On U2 by A1, A4, CLASSES1:42;
then On U1 in On U3 by A5, ORDINAL1:19;
hence U1 in U3 by A6, A3, CLASSES1:42; :: thesis: verum