let a, b be ordinal number ; :: 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 number such that
A0: ( c in dom (criticals f) & b = (criticals f) . c ) by Th06;
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 Th01;
then A6: 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 ThN3;
A7: dom (criticals f) = ord-type { c where c is Element of dom f : c is_a_fixpoint_of f } by ThN1;
b c/= (criticals f) . a by A1, EXCH1;
then c c/= a by A0, A3, A6, A7, Lem1;
then a in c by EXCH1;
then succ a c= c by ORDINAL1:21;
hence (criticals f) . (succ a) c= b by A0, ORDINAL4:9; :: thesis: verum