:: deftheorem defines criticals ORDINAL6:def 11 :
for g being Ordinal-Sequence-valued Sequence holds criticals g = numbering { a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) ) } ;