theorem Th19: :: CLASSES5:19

for U being Universe
for X being set
for n being non zero Nat st Funcs ((Seg n),{X}) is Element of U holds
X is Element of U