for b being Ordinal
for f being Ordinal-Sequence st b is_a_fixpoint_of f holds
ex a being Ordinal st
( a in dom (criticals f) & b = (criticals f) . a )