for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & ( for a being Ordinal st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ) holds
lims ((U -Veblen) | l) is continuous non-decreasing Ordinal-Sequence of U