let L be non empty complete Poset; 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:]; 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; verum