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 a' = 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 let x,
y be
Element of
S;
:: thesis: ( x <= y implies (Proj f,a) . x >= (Proj f,a) . y )assume A3:
x <= y
;
:: thesis: (Proj f,a) . x >= (Proj f,a) . yA4:
(Proj f,a) . x = f . a,
x
by Th7;
A5:
(Proj f,a) . y = f . a,
y
by Th7;
a' <= a'
;
then
[a',x] <= [a',y]
by A3, YELLOW_3:11;
hence
(Proj f,a) . x >= (Proj f,a) . y
by A1, A4, A5, WAYBEL_0:def 5;
:: thesis: verum end;
now let x,
y be
Element of
R;
:: thesis: ( x <= y implies (Proj f,b) . x >= (Proj f,b) . y )assume A6:
x <= y
;
:: thesis: (Proj f,b) . x >= (Proj f,b) . yA7:
(Proj f,b) . x = f . x,
b
by Th8;
A8:
(Proj f,b) . y = f . y,
b
by Th8;
reconsider b' =
b as
Element of
S ;
b' <= b'
;
then
[x,b'] <= [y,b']
by A6, YELLOW_3:11;
hence
(Proj f,b) . x >= (Proj f,b) . y
by A1, A7, A8, 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