for a being Ordinal
for l being limit_ordinal non empty Ordinal
for f being Ordinal-Sequence st l c= dom (criticals f) & a is_a_fixpoint_of f & ( for x being set st x in l holds
(criticals f) . x in a ) holds
l in dom (criticals f)