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 that
A2: f is monotone and
A3: 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;
hence f1 . x <= f1 . y by A1, A3, YELLOW_0:59; :: thesis: verum

end;