let a, b be Ordinal; :: 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
A1: a in dom (criticals f) and
A2: b is_a_fixpoint_of f and
A3: (criticals f) . a in b ; :: thesis: succ a in dom (criticals f)
consider c being Ordinal such that
A4: ( c in dom (criticals f) & b = (criticals f) . c ) by A2, Th33;
a in c by A1, A3, A4, Th23;
then succ a c= c by ORDINAL1:21;
hence succ a in dom (criticals f) by A4, ORDINAL1:12; :: thesis: verum