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 :: thesis: for x, y being Element of [:R,S:] st x <= y holds
f . x >= f . y

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;
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;
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:21;
hence f . x >= f . y by A8, A9, MCART_1:21; :: thesis: verum

end;

hence f is antitone ; :: thesis: verum