let L be non empty complete Poset; :: thesis: for D being non empty filtered Subset of [:L,L:] holds inf ((sup_op L) .: D) = inf ((proj1 D) "\/" (proj2 D))
let D be non empty filtered Subset of [:L,L:]; :: thesis: inf ((sup_op L) .: D) = inf ((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;
set D1 = proj1 D;
set D2 = proj2 D;
set f = sup_op L;
A1: ex_inf_of (sup_op L) .: D',L by YELLOW_0:17;
A2: ex_inf_of (proj1 D) "\/" (proj2 D),L by YELLOW_0:17;
A3: ex_inf_of uparrow ((sup_op L) .: D),L by YELLOW_0:17;
A4: (sup_op L) .: [:(proj1 D),(proj2 D):] c= (sup_op L) .: (uparrow D) by RELAT_1:156, YELLOW_3:49;
A5: (sup_op L) .: (uparrow D) c= uparrow ((sup_op L) .: D) by Th14;
(sup_op L) .: D' c= (sup_op L) .: [:(proj1 D),(proj2 D):] by RELAT_1:156, YELLOW_3:1;
then (sup_op L) .: D' c= (proj1 D) "\/" (proj2 D) by Th35;
then A6: inf ((sup_op L) .: D) >= inf ((proj1 D) "\/" (proj2 D)) by A1, A2, YELLOW_0:35;
(sup_op L) .: [:(proj1 D),(proj2 D):] = (proj1 D) "\/" (proj2 D) by Th35;
then inf ((proj1 D) "\/" (proj2 D)) >= inf (uparrow ((sup_op L) .: D)) by A2, A3, A4, A5, XBOOLE_1:1, YELLOW_0:35;
then inf ((proj1 D) "\/" (proj2 D)) >= inf ((sup_op L) .: D) by A1, WAYBEL_0:38;
hence inf ((sup_op L) .: D) = inf ((proj1 D) "\/" (proj2 D)) by A6, ORDERS_2:25; :: thesis: verum