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 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 antitone 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_9:def 1;
A6: Proj f,(x `1 ) is antitone 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_9:def 1;
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 antitone by WAYBEL_9:def 1; :: thesis: verum