set g = criticals f;
let a be Ordinal; :: according to ORDINAL2:def 13 :: thesis: for b₁ being set holds
( not a in dom (criticals f) or a = 0 or not a is limit_ordinal or not b₁ = (criticals f) . a or b₁ is_limes_of (criticals f) | a )
let b be Ordinal; :: thesis: ( not a in dom (criticals f) or a = 0 or not a is limit_ordinal or not b = (criticals f) . a or b is_limes_of (criticals f) | a )
reconsider h = (criticals f) | a as increasing Ordinal-Sequence by ORDINAL4:15;
assume A1: ( a in dom (criticals f) & a <> 0 & a is limit_ordinal & b = (criticals f) . a ) ; :: thesis: b is_limes_of (criticals f) | a
then A2: b = Union h by Th39;
a c= dom (criticals f) by A1, ORDINAL1:def 2;
then dom h = a by RELAT_1:62;
hence b is_limes_of (criticals f) | a by A1, A2, ORDINAL5:6; :: thesis: verum