let R, S, T be LATTICE; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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:]; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum