let f be Function of S,T; :: thesis: ( f is constant implies f is monotone )
assume A1: f is constant ; :: thesis: f is monotone
for x, y being Element of S st x <= y holds
f . x <= f . y

proof

let x, y be Element of S; :: thesis: ( x <= y implies f . x <= f . y )
assume x <= y ; :: thesis: f . x <= f . y
y in the carrier of S ;
then A2: y in dom f by FUNCT_2:def 1;
x in the carrier of S ;
then x in dom f by FUNCT_2:def 1;
hence f . x <= f . y by A1, A2, FUNCT_1:def 10; :: thesis: verum

end;

hence f is monotone by WAYBEL_1:def 2; :: thesis: verum