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