for a being Ordinal
for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & ( for c being Ordinal st c in l holds
a is_a_fixpoint_of (U -Veblen) . c ) holds
a is_a_fixpoint_of lims ((U -Veblen) | l)