theorem :: CLASSES5:20

for U being Universe
for X being set
for n being non zero Nat st n -tuples_on {X} is Element of U holds
X is Element of U