dom f = A by FUNCT_2:def 1;
hence ( f is c=-monotone implies for x, y being Element of A st x c= y holds
f . x c= f . y ) ; :: thesis: ( ( for x, y being Element of A st x c= y holds
f . x c= f . y ) implies f is c=-monotone )
assume A1: for x, y being Element of A st x c= y holds
f . x c= f . y ; :: thesis: f is c=-monotone
let x, y be set ; :: according to COHSP_1:def 11 :: thesis: ( not x in dom f or not y in dom f or not x c= y or f . x c= f . y )
assume ( x in dom f & y in dom f & x c= y ) ; :: thesis: f . x c= f . y
hence f . x c= f . y by A1; :: thesis: verum