let a, b be ordinal number ; :: thesis: for f being Ordinal-Sequence st a in dom (criticals f) & b is_a_fixpoint_of f & (criticals f) . a in b holds
succ a in dom (criticals f)
let f be Ordinal-Sequence; :: thesis: ( a in dom (criticals f) & b is_a_fixpoint_of f & (criticals f) . a in b implies succ a in dom (criticals f) )
set g = criticals f;
assume that
Z0: a in dom (criticals f) and
Z1: b is_a_fixpoint_of f and
Z2: (criticals f) . a in b ; :: thesis: succ a in dom (criticals f)
consider c being ordinal number such that
A1: ( c in dom (criticals f) & b = (criticals f) . c ) by Z1, Th06;
a in c by Z0, Z2, A1, ThN5;
then succ a c= c by ORDINAL1:21;
hence succ a in dom (criticals f) by A1, ORDINAL1:12; :: thesis: verum