let L be up-complete Semilattice; :: thesis: for D being non empty directed Subset of [:L,L:] holds sup ((inf_op L) .: D) = sup ((proj1 D) "/\" (proj2 D))
let D be non empty directed Subset of [:L,L:]; :: thesis: sup ((inf_op L) .: D) = sup ((proj1 D) "/\" (proj2 D))
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 YELLOW_3:21, YELLOW_3:22;
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= (inf_op L) .: (downarrow D) & (inf_op L) .: (downarrow D) c= downarrow ((inf_op L) .: D) ) by Th13, RELAT_1:123, YELLOW_3:48;
A4: (inf_op L) .: D is directed by YELLOW_2:15;
then A5: ex_sup_of (inf_op L) .: D,L by WAYBEL_0:75;
ex_sup_of downarrow ((inf_op L) .: D),L by A4, WAYBEL_0:75;
then sup (D1 "/\" D2) <= sup (downarrow ((inf_op L) .: D)) by A1, A3, A2, XBOOLE_1:1, YELLOW_0:34;
then A6: sup (D1 "/\" D2) <= sup ((inf_op L) .: D) by A5, WAYBEL_0:33;
(inf_op L) .: D9 c= (inf_op L) .: [:D1,D2:] by RELAT_1:123, YELLOW_3:1;
then (inf_op L) .: D9 c= D1 "/\" D2 by Th32;
then sup ((inf_op L) .: D) <= sup (D1 "/\" D2) by A5, A1, YELLOW_0:34;
hence sup ((inf_op L) .: D) = sup ((proj1 D) "/\" (proj2 D)) by A6, ORDERS_2:2; :: thesis: verum