let R, S, T be LATTICE; :: thesis: for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj f,a is monotone & Proj f,b is monotone ) ) holds
f is monotone
let f be Function of [:R,S:],T; :: thesis: ( ( for a being Element of R
for b being Element of S holds
( Proj f,a is monotone & Proj f,b is monotone ) ) implies f is monotone )
assume A1: for a being Element of R
for b being Element of S holds
( Proj f,a is monotone & Proj f,b is monotone ) ; :: thesis: f is monotone

now

let x, y be Element of [:R,S:]; :: thesis: ( x <= y implies f . x <= f . y )
assume x <= y ; :: thesis: f . x <= f . y
then A2: ( x `1 <= y `1 & x `2 <= y `2 ) by YELLOW_3:12;
A3: Proj f,(y `2 ) is monotone by A1;
A4: f . (x `1 ),(y `2 ) = (Proj f,(y `2 )) . (x `1 ) by Th8;
f . (y `1 ),(y `2 ) = (Proj f,(y `2 )) . (y `1 ) by Th8;
then A5: f . [(x `1 ),(y `2 )] <= f . [(y `1 ),(y `2 )] by A2, A3, A4, WAYBEL_1:def 2;
A6: Proj f,(x `1 ) is monotone by A1;
A7: f . (x `1 ),(x `2 ) = (Proj f,(x `1 )) . (x `2 ) by Th7;
f . (x `1 ),(y `2 ) = (Proj f,(x `1 )) . (y `2 ) by Th7;
then f . [(x `1 ),(x `2 )] <= f . [(x `1 ),(y `2 )] by A2, A6, A7, WAYBEL_1:def 2;
then A8: f . [(x `1 ),(x `2 )] <= f . [(y `1 ),(y `2 )] by A5, YELLOW_0:def 2;
A9: [:the carrier of R,the carrier of S:] = the carrier of [:R,S:] by YELLOW_3:def 2;
then f . [(y `1 ),(y `2 )] = f . y by MCART_1:23;
hence f . x <= f . y by A8, A9, MCART_1:23; :: thesis: verum

end;

hence f is monotone by WAYBEL_1:def 2; :: thesis: verum