let L be up-complete Semilattice; :: thesis: ( ( 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) ; :: thesis: 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; :: thesis: (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 ;

:: thesis: verum

assume A1: for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ; :: thesis: 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; :: thesis: (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 ;

:: thesis: verum