let L be up-complete Semilattice; ( ( for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) implies for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) )
assume A1:
for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2)
; for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
let D1, D2 be non empty directed Subset of L; (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
A2:
ex_sup_of D2,L
by WAYBEL_0:75;
A3:
ex_sup_of (downarrow D1) "/\" (downarrow D2),L
by WAYBEL_0:75;
A4:
ex_sup_of D1 "/\" D2,L
by WAYBEL_0:75;
ex_sup_of D1,L
by WAYBEL_0:75;
hence (sup D1) "/\" (sup D2) =
(sup (downarrow D1)) "/\" (sup D2)
by WAYBEL_0:33
.=
(sup (downarrow D1)) "/\" (sup (downarrow D2))
by A2, WAYBEL_0:33
.=
sup ((downarrow D1) "/\" (downarrow D2))
by A1
.=
sup (downarrow ((downarrow D1) "/\" (downarrow D2)))
by A3, WAYBEL_0:33
.=
sup (downarrow (D1 "/\" D2))
by YELLOW_4:62
.=
sup (D1 "/\" D2)
by A4, WAYBEL_0:33
;
verum