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 antitone & Proj f,b is antitone ) ) holds
f is antitone
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 antitone & Proj f,b is antitone ) ) implies f is antitone )
assume A1: for a being Element of R
for b being Element of S holds
( Proj f,a is antitone & Proj f,b is antitone ) ; :: thesis: f is antitone

now

let x, y be Element of [:R,S:]; :: thesis: ( x <= y implies f . x >= f . y )
assume A2: x <= y ; :: thesis: f . x >= f . y
then A3: x `1 <= y `1 by YELLOW_3:12;
A4: x `2 <= y `2 by A2, YELLOW_3:12;
A5: f . (x `1 ),(y `2 ) = (Proj f,(x `1 )) . (y `2 ) by Th7;
( Proj f,(x `1 ) is antitone & f . (x `1 ),(x `2 ) = (Proj f,(x `1 )) . (x `2 ) ) by A1, Th7;
then A6: f . [(x `1 ),(x `2 )] >= f . [(x `1 ),(y `2 )] by A4, A5, WAYBEL_9:def 1;
A7: f . (y `1 ),(y `2 ) = (Proj f,(y `2 )) . (y `1 ) by Th8;
( Proj f,(y `2 ) is antitone & f . (x `1 ),(y `2 ) = (Proj f,(y `2 )) . (x `1 ) ) by A1, Th8;
then f . [(x `1 ),(y `2 )] >= f . [(y `1 ),(y `2 )] by A3, A7, WAYBEL_9:def 1;
then A8: f . [(x `1 ),(x `2 )] >= f . [(y `1 ),(y `2 )] by A6, 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 antitone by WAYBEL_9:def 1; :: thesis: verum