let L be up-complete LATTICE; :: thesis: ( L is meet-continuous iff for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) )

hereby :: thesis: ( ( for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ) implies L is meet-continuous )

assume L is meet-continuous ; :: thesis: for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
then for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) by Th50;
hence for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th40; :: thesis: verum

end;

assume for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ; :: thesis: L is meet-continuous
hence ( L is up-complete & L is satisfying_MC ) by Th44; :: according to WAYBEL_2:def 7 :: thesis: verum