let R, S, T be LATTICE; for f being monotone Function of [:R,S:],T
for a being Element of R
for b being Element of S
for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds
f . [a,b] <= sup (f .: X)
let f be monotone Function of [:R,S:],T; for a being Element of R
for b being Element of S
for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds
f . [a,b] <= sup (f .: X)
let a be Element of R; for b being Element of S
for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds
f . [a,b] <= sup (f .: X)
let b be Element of S; for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds
f . [a,b] <= sup (f .: X)
let X be directed Subset of [:R,S:]; ( ex_sup_of f .: X,T & a in proj1 X & b in proj2 X implies f . [a,b] <= sup (f .: X) )
assume that
A1:
ex_sup_of f .: X,T
and
A2:
a in proj1 X
and
A3:
b in proj2 X
; f . [a,b] <= sup (f .: X)
consider d being object such that
A4:
[d,b] in X
by A3, XTUPLE_0:def 13;
d in proj1 X
by A4, XTUPLE_0:def 12;
then reconsider d = d as Element of R ;
consider c being object such that
A5:
[a,c] in X
by A2, XTUPLE_0:def 12;
c in proj2 X
by A5, XTUPLE_0:def 13;
then reconsider c = c as Element of S ;
consider z being Element of [:R,S:] such that
A6:
z in X
and
A7:
( [a,c] <= z & [d,b] <= z )
by A5, A4, WAYBEL_0:def 1;
A8:
f .: X is_<=_than sup (f .: X)
by A1, YELLOW_0:30;
[a,c] "\/" [d,b] <= z "\/" z
by A7, YELLOW_3:3;
then
[a,c] "\/" [d,b] <= z
by YELLOW_5:1;
then
[(a "\/" d),(c "\/" b)] <= z
by YELLOW10:16;
then A9:
f . [(a "\/" d),(c "\/" b)] <= f . z
by WAYBEL_1:def 2;
dom f = the carrier of [:R,S:]
by FUNCT_2:def 1;
then
f . z in f .: X
by A6, FUNCT_1:def 6;
then A10:
f . z <= sup (f .: X)
by A8;
( a <= a "\/" d & b <= c "\/" b )
by YELLOW_0:22;
then
[a,b] <= [(a "\/" d),(c "\/" b)]
by YELLOW_3:11;
then
f . [a,b] <= f . [(a "\/" d),(c "\/" b)]
by WAYBEL_1:def 2;
then
f . [a,b] <= f . z
by A9, YELLOW_0:def 2;
hence
f . [a,b] <= sup (f .: X)
by A10, YELLOW_0:def 2; verum