let a, b be Ordinal; :: thesis: for f being Ordinal-Sequence st succ a in dom (criticals f) & b is_a_fixpoint_of f & (criticals f) . a in b holds
(criticals f) . (succ a) c= b
let f be Ordinal-Sequence; :: thesis: ( succ a in dom (criticals f) & b is_a_fixpoint_of f & (criticals f) . a in b implies (criticals f) . (succ a) c= b )
set g = criticals f;
set Y = { c where c is Element of dom f : c is_a_fixpoint_of f } ;
set X = ord-type { c where c is Element of dom f : c is_a_fixpoint_of f } ;
assume A1: ( succ a in dom (criticals f) & b is_a_fixpoint_of f & (criticals f) . a in b ) ; :: thesis: (criticals f) . (succ a) c= b
then consider c being Ordinal such that
A2: ( c in dom (criticals f) & b = (criticals f) . c ) by Th33;
a in succ a by ORDINAL1:6;
then A3: ( a in dom (criticals f) & (criticals f) . a in (criticals f) . (succ a) ) by A1, ORDINAL1:10, ORDINAL2:def 12;
On { c where c is Element of dom f : c is_a_fixpoint_of f } = { c where c is Element of dom f : c is_a_fixpoint_of f } by Th28;
then A4: criticals f is_isomorphism_of RelIncl (ord-type { c where c is Element of dom f : c is_a_fixpoint_of f } ), RelIncl { c where c is Element of dom f : c is_a_fixpoint_of f } by Th21;
A5: dom (criticals f) = ord-type { c where c is Element of dom f : c is_a_fixpoint_of f } by Th18;
b c/= (criticals f) . a by A1, Th4;
then c c/= a by A2, A3, A4, A5, Th6;
then a in c by Th4;
then succ a c= c by ORDINAL1:21;
hence (criticals f) . (succ a) c= b by A2, ORDINAL4:9; :: thesis: verum