let L be up-complete Semilattice; :: thesis: for D being non empty directed Subset of [:L,L:] holds sup (() .: D) = sup (() "/\" ())
let D be non empty directed Subset of [:L,L:]; :: thesis: sup (() .: D) = sup (() "/\" ())
reconsider C = the carrier of L as non empty set ;
reconsider D9 = D as non empty Subset of [:C,C:] by YELLOW_3:def 2;
reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by ;
set f = inf_op L;
A1: ex_sup_of D1 "/\" D2,L by WAYBEL_0:75;
A2: (inf_op L) .: [:D1,D2:] = D1 "/\" D2 by Th32;
A3: ( (inf_op L) .: [:D1,D2:] c= () .: () & () .: () c= downarrow (() .: D) ) by ;
A4: (inf_op L) .: D is directed by YELLOW_2:15;
then A5: ex_sup_of () .: D,L by WAYBEL_0:75;
ex_sup_of downarrow (() .: D),L by ;
then sup (D1 "/\" D2) <= sup (downarrow (() .: D)) by ;
then A6: sup (D1 "/\" D2) <= sup (() .: D) by ;
(inf_op L) .: D9 c= () .: [:D1,D2:] by ;
then (inf_op L) .: D9 c= D1 "/\" D2 by Th32;
then sup (() .: D) <= sup (D1 "/\" D2) by ;
hence sup (() .: D) = sup (() "/\" ()) by ; :: thesis: verum