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

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