let L be up-complete Semilattice; 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:]; 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; verum