theorem :: CLASSES5:23

for U1, U2 being Universe st U1 in U2 holds
for x being Set of U1 holds x is Set of U2