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 ) by COHSP_1:def 12; :: 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 12 :: thesis: ( not x in proj1 f or not y in proj1 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