theorem :: CLASSES5:36

for U1, U2 being Universe st U1 in U2 holds
for x being object st x is U1 -Class holds
x is U2 -set