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