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 dom f or not y in dom f or not x c= y or f . x c= f . y )
assume A1: ( x in dom f & y in dom f & x c= y ) ; :: thesis: f . x c= f . y
then f . x = b by FUNCOP_1:13
.= f . y by A1, FUNCOP_1:13 ;
hence f . x c= f . y ; :: thesis: verum