set f = S --> a;
for x, y being Element of S st x <= y holds
(S --> a) . x <= (S --> a) . y
proof
let x, y be Element of S; :: thesis: ( x <= y implies (S --> a) . x <= (S --> a) . y )
assume x <= y ; :: thesis: (S --> a) . x <= (S --> a) . y
(S --> a) . x = ( the carrier of S --> a) . x
.= a by FUNCOP_1:7
.= ( the carrier of S --> a) . y by FUNCOP_1:7
.= (S --> a) . y ;
hence (S --> a) . x <= (S --> a) . y ; :: thesis: verum
end;
hence S --> a is monotone by WAYBEL_1:def 2; :: thesis: verum