let S be non empty RelStr ; :: thesis:
let T, T1 be non empty RelStr ; :: thesis:
assume A1: T is SubRelStr of T1 ; :: thesis:
let f be Function of S,T; :: thesis:
let f1 be Function of S,T1; :: thesis:
assume that
A2: f is monotone and
A3: f = f1 ; :: thesis:
thus f1 is monotone :: thesis:

let x, y be Element of S; :: according to WAYBEL_1:def 2 :: thesis:
assume x <= y ; :: thesis:
then f . x <= f . y by A2;
hence f1 . x <= f1 . y by A1, A3, YELLOW_0:59; :: thesis:

end;