let n be Nat; :: thesis: UNIVERSE n in UNIVERSE (n + 1)
succ (Segm n) = Segm (n + 1) by NAT_1:38;
then UNIVERSE (n + 1) = Tarski-Class (UNIVERSE n) by CLASSES2:66
.= GrothendieckUniverse (UNIVERSE n) by CLASSES3:22 ;
hence UNIVERSE n in UNIVERSE (n + 1) by CLASSES3:def 4; :: thesis: verum