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 c being set such that
A4: [a,c] in X by A2, RELAT_1:def 4;
c in proj2 X by A4, RELAT_1:def 5;
then reconsider c = c as Element of S ;
consider d being set such that
A5: [d,b] in X by A3, RELAT_1:def 5;
d in proj1 X by A5, RELAT_1:def 4;
then reconsider d = d as Element of R ;
consider z being Element of [:R,S:] such that
A6: ( z in X & [a,c] <= z & [d,b] <= z ) by A4, A5, WAYBEL_0:def 1;
[a,c] "\/" [d,b] <= z "\/" z by A6, YELLOW_3:3;
then [a,c] "\/" [d,b] <= z by YELLOW_5:1;
then A7: [(a "\/" d),(c "\/" b)] <= z by YELLOW10:16;
( a <= a "\/" d & b <= c "\/" b ) by YELLOW_0:22;
then [a,b] <= [(a "\/" d),(c "\/" b)] by YELLOW_3:11;
then A8: f . [a,b] <= f . [(a "\/" d),(c "\/" b)] by WAYBEL_1:def 2;
f . [(a "\/" d),(c "\/" b)] <= f . z by A7, WAYBEL_1:def 2;
then A9: f . [a,b] <= f . z by A8, YELLOW_0:def 2;
dom f = the carrier of [:R,S:] by FUNCT_2:def 1;
then A10: f . z in f .: X by A6, FUNCT_1:def 12;
f .: X is_<=_than sup (f .: X) by A1, YELLOW_0:30;
then f . z <= sup (f .: X) by A10, LATTICE3:def 9;
hence f . [a,b] <= sup (f .: X) by A9, YELLOW_0:def 2; :: thesis: verum