let R, S, T be non empty reflexive RelStr ; 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; 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; 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; ( 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
; ( Proj (f,a) is antitone & Proj (f,b) is antitone )
A2:
now for x, y being Element of R st x <= y holds
(Proj (f,b)) . x >= (Proj (f,b)) . yreconsider b9 =
b as
Element of
S ;
let x,
y be
Element of
R;
( 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
;
(Proj (f,b)) . x >= (Proj (f,b)) . ythen
[x,b9] <= [y,b9]
by A3, YELLOW_3:11;
hence
(Proj (f,b)) . x >= (Proj (f,b)) . y
by A1, A4;
verum end;
now for x, y being Element of S st x <= y holds
(Proj (f,a)) . x >= (Proj (f,a)) . ylet x,
y be
Element of
S;
( 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
;
(Proj (f,a)) . x >= (Proj (f,a)) . ythen
[a9,x] <= [a9,y]
by A5, YELLOW_3:11;
hence
(Proj (f,a)) . x >= (Proj (f,a)) . y
by A1, A6;
verum end;
hence
( Proj (f,a) is antitone & Proj (f,b) is antitone )
by A2; verum