theorem Th69: :: CLASSES4:69

for UN being Universe
for X being set st X in UN holds
for s being FinSequence of X holds s in UN