theorem Th52: :: ORDINAL6:52

for l being limit_ordinal non empty Ordinal
for g being Ordinal-Sequence-valued Sequence st dom g <> {} & ( for a being Ordinal st a in dom g holds
g . a is normal ) & l in dom (criticals g) holds
(criticals g) . l = Union ((criticals g) | l)