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 D9 = 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 (proj1 D) "\/" (proj2 D),L by YELLOW_0:17;
A2: ( ex_inf_of uparrow ((sup_op L) .: D),L & (sup_op L) .: [:(proj1 D),(proj2 D):] c= (sup_op L) .: (uparrow D) ) by RELAT_1:123, YELLOW_0:17, YELLOW_3:49;
( (sup_op L) .: (uparrow D) c= uparrow ((sup_op L) .: D) & (sup_op L) .: [:(proj1 D),(proj2 D):] = (proj1 D) "\/" (proj2 D) ) by Th14, Th35;
then inf ((proj1 D) "\/" (proj2 D)) >= inf (uparrow ((sup_op L) .: D)) by A1, A2, XBOOLE_1:1, YELLOW_0:35;
then A3: inf ((proj1 D) "\/" (proj2 D)) >= inf ((sup_op L) .: D) by WAYBEL_0:38, YELLOW_0:17;
(sup_op L) .: D9 c= (sup_op L) .: [:(proj1 D),(proj2 D):] by RELAT_1:123, YELLOW_3:1;
then ( ex_inf_of (sup_op L) .: D9,L & (sup_op L) .: D9 c= (proj1 D) "\/" (proj2 D) ) by Th35, YELLOW_0:17;
then inf ((sup_op L) .: D) >= inf ((proj1 D) "\/" (proj2 D)) by A1, YELLOW_0:35;
hence inf ((sup_op L) .: D) = inf ((proj1 D) "\/" (proj2 D)) by A3, ORDERS_2:2; :: thesis: verum