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) )

hence ( L is up-complete & L is satisfying_MC ) by Th44; :: according to WAYBEL_2:def 7 :: thesis: verum

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
for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
; :: thesis: 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;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

hence ( L is up-complete & L is satisfying_MC ) by Th44; :: according to WAYBEL_2:def 7 :: thesis: verum