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

proof

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

end;