let S be non empty RelStr ; :: thesis: for T, T1 being non empty RelStr st T is SubRelStr of T1 holds
for f being Function of S,T
for f1 being Function of S,T1 st f is monotone & f = f1 holds
f1 is monotone
let T, T1 be non empty RelStr ; :: thesis: ( T is SubRelStr of T1 implies for f being Function of S,T
for f1 being Function of S,T1 st f is monotone & f = f1 holds
f1 is monotone )
assume A1: T is SubRelStr of T1 ; :: thesis: for f being Function of S,T
for f1 being Function of S,T1 st f is monotone & f = f1 holds
f1 is monotone
let f be Function of S,T; :: thesis: for f1 being Function of S,T1 st f is monotone & f = f1 holds
f1 is monotone
let f1 be Function of S,T1; :: thesis: ( f is monotone & f = f1 implies f1 is monotone )
assume A2: ( f is monotone & f = f1 ) ; :: thesis: f1 is monotone
thus f1 is monotone :: thesis: verum

proof

let x, y be Element of S; :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or f1 . x <= f1 . y )
assume x <= y ; :: thesis: f1 . x <= f1 . y
then f . x <= f . y by A2, WAYBEL_1:def 2;
hence f1 . x <= f1 . y by A1, A2, YELLOW_0:60; :: thesis: verum

end;