let g be Ordinal-Sequence-valued T-Sequence; :: thesis: ( dom g <> {} & ( for a being ordinal number st a in dom g holds
g . a is normal ) implies criticals g is continuous )
assume Z0: dom g <> {} ; :: thesis: ( ex a being ordinal number st
( a in dom g & not g . a is normal ) or criticals g is continuous )
assume Z1: for a being ordinal number st a in dom g holds
g . a is normal ; :: thesis: criticals g is continuous
set f = criticals g;
let a be ordinal number ; :: according to ORDINAL2:def 13 :: thesis: for b₁ being set holds
( not a in proj1 (criticals g) or a = {} or not a is limit_ordinal or not b₁ = (criticals g) . a or b₁ is_limes_of (criticals g) | a )
let b be ordinal number ; :: thesis: ( not a in proj1 (criticals g) or a = {} or not a is limit_ordinal or not b = (criticals g) . a or b is_limes_of (criticals g) | a )
reconsider h = (criticals g) | a as increasing Ordinal-Sequence by ORDINAL4:15;
assume A1: ( a in dom (criticals g) & a <> {} & a is limit_ordinal & b = (criticals g) . a ) ; :: thesis: b is_limes_of (criticals g) | a
then A2: b = Union h by Z0, Z1, ThA9;
a c= dom (criticals g) by A1, ORDINAL1:def 2;
then dom h = a by RELAT_1:62;
hence b is_limes_of (criticals g) | a by A1, A2, ORDINAL5:6; :: thesis: verum