:: deftheorem defines criticals ORDINAL6:def 7 :
for f being Ordinal-Sequence holds criticals f = numbering { a where a is Element of dom f : a is_a_fixpoint_of f } ;