theorem :: ORDINAL6:51

for a being Ordinal
for l being limit_ordinal non empty Ordinal
for g being Ordinal-Sequence-valued Sequence st dom g <> {} & l c= dom (criticals g) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) & ( for x being set st x in l holds
(criticals g) . x in a ) holds
l in dom (criticals g)