set b = the Element of B;
reconsider f = A --> the Element of B as Function of A,B ;
take f ; :: 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 that
A1: x in dom f and
A2: y in dom f and
x c= y ; :: thesis: f . x c= f . y
f . x = the Element of B by A1, FUNCOP_1:7
.= f . y by A2, FUNCOP_1:7 ;
hence f . x c= f . y ; :: thesis: verum