theorem :: CLASSES5:22

for U1, U2 being Universe st U1 in U2 holds
for x being object st x is U1 -set holds
x is U2 -set by CLASSES4:def 1;