for A being Ordinal
for L being Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = UNIVERSE B ) holds
UNIVERSE A = Universe_closure (Union L) by Lm6;