let R, S, T be non empty reflexive RelStr ; :: thesis: for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S st f is monotone holds
( Proj f,a is monotone & Proj f,b is monotone )
let f be Function of [:R,S:],T; :: thesis: for a being Element of R
for b being Element of S st f is monotone holds
( Proj f,a is monotone & Proj f,b is monotone )
let a be Element of R; :: thesis: for b being Element of S st f is monotone holds
( Proj f,a is monotone & Proj f,b is monotone )
let b be Element of S; :: thesis: ( f is monotone implies ( Proj f,a is monotone & Proj f,b is monotone ) )
reconsider a = a as Element of R ;
reconsider b = b as Element of S ;
set g = Proj f,b;
set h = Proj f,a;
assume A1: f is monotone ; :: thesis: ( Proj f,a is monotone & Proj f,b is monotone )

A2: now

let x, y be Element of R; :: thesis: ( x <= y implies (Proj f,b) . x <= (Proj f,b) . y )
A3: b <= b ;
A4: ( (Proj f,b) . x = f . x,b & (Proj f,b) . y = f . y,b ) by Th8;
assume x <= y ; :: thesis: (Proj f,b) . x <= (Proj f,b) . y
then [x,b] <= [y,b] by A3, YELLOW_3:11;
hence (Proj f,b) . x <= (Proj f,b) . y by A1, A4, WAYBEL_1:def 2; :: thesis: verum

end;

now

let x, y be Element of S; :: thesis: ( x <= y implies (Proj f,a) . x <= (Proj f,a) . y )
A5: a <= a ;
A6: ( (Proj f,a) . x = f . a,x & (Proj f,a) . y = f . a,y ) by Th7;
assume x <= y ; :: thesis: (Proj f,a) . x <= (Proj f,a) . y
then [a,x] <= [a,y] by A5, YELLOW_3:11;
hence (Proj f,a) . x <= (Proj f,a) . y by A1, A6, WAYBEL_1:def 2; :: thesis: verum

end;

hence ( Proj f,a is monotone & Proj f,b is monotone ) by A2, WAYBEL_1:def 2; :: thesis: verum