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 :: thesis: for x, y being Element of R st x <= y holds
(Proj (f,b)) . x <= (Proj (f,b)) . y

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 :: thesis: for x, y being Element of S st x <= y holds
(Proj (f,a)) . x <= (Proj (f,a)) . y

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