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 monotone holds
( Proj f,a is monotone & Proj f,b is monotone )
let f be Function of [:R,S:],T; :: thesis: for a being Element of R
for b being Element of S st f is monotone holds
( Proj f,a is monotone & Proj f,b is monotone )
let a be Element of R; :: thesis: for b being Element of S st f is monotone holds
( Proj f,a is monotone & Proj f,b is monotone )
let b be Element of S; :: thesis: ( f is monotone implies ( Proj f,a is monotone & Proj f,b is monotone ) )
reconsider a = a as Element of R ;
reconsider b = b as Element of S ;
set g = Proj f,b;
set h = Proj f,a;
assume A1:
f is monotone
; :: thesis: ( Proj f,a is monotone & Proj f,b is monotone )
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_1:def 2;
:: 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;
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_1:def 2;
:: thesis: verum end;
hence
( Proj f,a is monotone & Proj f,b is monotone )
by A2, WAYBEL_1:def 2; :: thesis: verum