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

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