let f1, f2 be Ordinal-Sequence; :: thesis: ( f1 c= f2 implies criticals f1 c= criticals f2 )
assume A1: f1 c= f2 ; :: thesis: criticals f1 c= criticals f2
then A2: dom f1 c= dom f2 by GRFUNC_1:2;
set X = { a where a is Element of dom f1 : a is_a_fixpoint_of f1 } ;
set Z = { a where a is Element of dom f2 : a is_a_fixpoint_of f2 } ;
( On { a where a is Element of dom f1 : a is_a_fixpoint_of f1 } = { a where a is Element of dom f1 : a is_a_fixpoint_of f1 } & On { a where a is Element of dom f2 : a is_a_fixpoint_of f2 } = { a where a is Element of dom f2 : a is_a_fixpoint_of f2 } ) by Th28;
then reconsider X = { a where a is Element of dom f1 : a is_a_fixpoint_of f1 } , Z = { a where a is Element of dom f2 : a is_a_fixpoint_of f2 } as ordinal-membered set ;
set Y = Z \ X;

A3: now :: thesis: for x, y being set st x in X & y in Z \ X holds
x in y

let x, y be set ; :: thesis: ( x in X & y in Z \ X implies x in y )
assume x in X ; :: thesis: ( y in Z \ X implies x in y )
then consider a being Element of dom f1 such that
A4: ( x = a & a is_a_fixpoint_of f1 ) ;
assume y in Z \ X ; :: thesis: x in y
then A5: ( y in Z & not y in X ) by XBOOLE_0:def 5;
then consider b being Element of dom f2 such that
A6: ( y = b & b is_a_fixpoint_of f2 ) ;

now :: thesis: not b in dom f1

assume A7: b in dom f1 ; :: thesis: contradiction
then f1 . b = f2 . b by A1, GRFUNC_1:2
.= b by A6 ;
then b is_a_fixpoint_of f1 by A7;
hence contradiction by A5, A6; :: thesis: verum

end;

then ( dom f1 c= b & x in dom f1 ) by A4, Th4;
hence x in y by A6; :: thesis: verum

end;

X c= Z

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Z )
assume x in X ; :: thesis: x in Z
then consider a being Element of dom f1 such that
A8: ( x = a & a is_a_fixpoint_of f1 ) ;
( a in dom f1 & a = f1 . a ) by A8;
then ( a in dom f2 & a = f2 . a ) by A1, A2, GRFUNC_1:2;
then a is_a_fixpoint_of f2 ;
hence x in Z by A8; :: thesis: verum

end;

then X \/ (Z \ X) = Z by XBOOLE_1:45;
then criticals f2 = (criticals f1) ^ (numbering (Z \ X)) by A3, Th25;
hence criticals f1 c= criticals f2 by Th9; :: thesis: verum