let f1, f2 be Ordinal-Sequence; :: thesis: ( f1 c= f2 implies criticals f1 c= criticals f2 )
assume Z0: f1 c= f2 ; :: thesis: criticals f1 c= criticals f2
then Z1: 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 Th01;
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;

A1: now

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
B1: ( x = a & a is_a_fixpoint_of f1 ) ;
assume y in Z \ X ; :: thesis: x in y
then B2: ( y in Z & not y in X ) by XBOOLE_0:def 5;
then consider b being Element of dom f2 such that
B3: ( y = b & b is_a_fixpoint_of f2 ) ;

now

assume B4: b in dom f1 ; :: thesis: contradiction
then f1 . b = f2 . b by Z0, GRFUNC_1:2
.= b by B3, ABIAN:def 3 ;
then b is_a_fixpoint_of f1 by B4, ABIAN:def 3;
hence contradiction by B2, B3, B4; :: thesis: verum

end;

then ( dom f1 c= b & x in dom f1 ) by B1, EXCH1, ABIAN:def 3;
hence x in y by B3; :: thesis: verum

end;

X c= Z

proof

let x be set ; :: 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
B1: ( x = a & a is_a_fixpoint_of f1 ) ;
B6: ( a in dom f1 & a = f1 . a ) by B1, ABIAN:def 3;
then ( a in dom f2 & a = f2 . a ) by Z0, Z1, GRFUNC_1:2;
then a is_a_fixpoint_of f2 by ABIAN:def 3;
hence x in Z by B1, B6, Z1; :: thesis: verum

end;

then X \/ (Z \ X) = Z by XBOOLE_1:45;
then criticals f2 = (criticals f1) ^ (numbering (Z \ X)) by A1, ThN7;
hence criticals f1 c= criticals f2 by Lem4; :: thesis: verum