theorem Th30: :: ORDINAL6:30

for f being Ordinal-Sequence holds
( rng (criticals f) = { a where a is Element of dom f : a is_a_fixpoint_of f } & rng (criticals f) c= rng f )