for a, b being set st a in dom (f | X) & b in dom (f | X) & a c= b holds
(f | X) . a c= (f | X) . b

proof

let a, b be set ; :: thesis: ( a in dom (f | X) & b in dom (f | X) & a c= b implies (f | X) . a c= (f | X) . b )
assume that
A1: ( a in dom (f | X) & b in dom (f | X) ) and
A2: a c= b ; :: thesis: (f | X) . a c= (f | X) . b
( a in dom f & b in dom f ) by A1, RELAT_1:57;
then ( (f | X) . a = f . a & f . a c= f . b ) by A1, A2, COHSP_1:def 11, FUNCT_1:47;
hence (f | X) . a c= (f | X) . b by A1, FUNCT_1:47; :: thesis: verum

end;

hence f | X is c=-monotone by COHSP_1:def 11; :: thesis: verum