theorem :: CLASSES5:47

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