theorem :: CLASSES5:46

for U being Universe
for X being Set of U
for Y being set st Y in X holds
Y is Set of U