let a be ordinal number ; :: thesis: for l being limit_ordinal non empty Ordinal
for f being Ordinal-Sequence st l c= dom (criticals f) & a is_a_fixpoint_of f & ( for x being set st x in l holds
(criticals f) . x in a ) holds
l in dom (criticals f)
let l be limit_ordinal non empty Ordinal; :: thesis: for f being Ordinal-Sequence st l c= dom (criticals f) & a is_a_fixpoint_of f & ( for x being set st x in l holds
(criticals f) . x in a ) holds
l in dom (criticals f)
let f be Ordinal-Sequence; :: thesis: ( l c= dom (criticals f) & a is_a_fixpoint_of f & ( for x being set st x in l holds
(criticals f) . x in a ) implies l in dom (criticals f) )
set g = criticals f;
assume that
Z1: l c= dom (criticals f) and
Z2: a is_a_fixpoint_of f and
Z4: for x being set st x in l holds
(criticals f) . x in a ; :: thesis: l in dom (criticals f)
consider b being ordinal number such that
A1: ( b in dom (criticals f) & a = (criticals f) . b ) by Z2, Th06;
l c= b

proof

let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in l or x in b )
assume x in l ; :: thesis: x in b
then ( x in dom (criticals f) & (criticals f) . x in (criticals f) . b ) by Z1, Z4, A1;
hence x in b by A1, ThN5; :: thesis: verum

end;

hence l in dom (criticals f) by A1, ORDINAL1:12; :: thesis: verum