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

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, WAYBEL_0:def 5; :: thesis: verum

end;

now

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, WAYBEL_0:def 5; :: thesis: verum

end;

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