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 antitone holds
( Proj (f,a) is antitone & Proj (f,b) is antitone )
let f be Function of [:R,S:],T; :: thesis: for a being Element of R
for b being Element of S st f is antitone holds
( Proj (f,a) is antitone & Proj (f,b) is antitone )
let a be Element of R; :: thesis: for b being Element of S st f is antitone holds
( Proj (f,a) is antitone & Proj (f,b) is antitone )
let b be Element of S; :: thesis: ( f is antitone implies ( Proj (f,a) is antitone & Proj (f,b) is antitone ) )
reconsider a9 = a as Element of R ;
set g = Proj (f,b);
set h = Proj (f,a);
assume A1: f is antitone ; :: thesis: ( Proj (f,a) is antitone & Proj (f,b) is antitone )

A2: now :: thesis: for x, y being Element of R st x <= y holds
(Proj (f,b)) . x >= (Proj (f,b)) . y

reconsider b9 = b as Element of S ;
let x, y be Element of R; :: thesis: ( x <= y implies (Proj (f,b)) . x >= (Proj (f,b)) . y )
A3: b9 <= b9 ;
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,b9] <= [y,b9] by A3, YELLOW_3:11;
hence (Proj (f,b)) . x >= (Proj (f,b)) . y by A1, A4; :: 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: a9 <= a9 ;
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 [a9,x] <= [a9,y] by A5, YELLOW_3:11;
hence (Proj (f,a)) . x >= (Proj (f,a)) . y by A1, A6; :: thesis: verum

end;

hence ( Proj (f,a) is antitone & Proj (f,b) is antitone ) by A2; :: thesis: verum