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 D' = 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: (inf_op L) .: D is directed by YELLOW_2:17;
then A2: ex_sup_of (inf_op L) .: D,L by WAYBEL_0:75;
A3: ex_sup_of D1 "/\" D2,L by WAYBEL_0:75;
downarrow ((inf_op L) .: D) is directed by A1;
then A4: ex_sup_of downarrow ((inf_op L) .: D),L by WAYBEL_0:75;
A5: (inf_op L) .: [:D1,D2:] c= (inf_op L) .: (downarrow D) by RELAT_1:156, YELLOW_3:48;
A6: (inf_op L) .: (downarrow D) c= downarrow ((inf_op L) .: D) by Th13;
(inf_op L) .: D' c= (inf_op L) .: [:D1,D2:] by RELAT_1:156, YELLOW_3:1;
then (inf_op L) .: D' c= D1 "/\" D2 by Th32;
then A7: sup ((inf_op L) .: D) <= sup (D1 "/\" D2) by A2, A3, YELLOW_0:34;
(inf_op L) .: [:D1,D2:] = D1 "/\" D2 by Th32;
then sup (D1 "/\" D2) <= sup (downarrow ((inf_op L) .: D)) by A3, A4, A5, A6, XBOOLE_1:1, YELLOW_0:34;
then sup (D1 "/\" D2) <= sup ((inf_op L) .: D) by A2, WAYBEL_0:33;
hence sup ((inf_op L) .: D) = sup ((proj1 D) "/\" (proj2 D)) by A7, ORDERS_2:25; :: thesis: verum