let L be up-complete Semilattice; :: thesis: ( L is meet-continuous iff inf_op L is directed-sups-preserving )
hereby :: thesis: ( inf_op L is directed-sups-preserving implies L is meet-continuous )
assume L is meet-continuous ; :: thesis: inf_op L is directed-sups-preserving
then for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x <= sup ({x} "/\" D) by Th45;
hence inf_op L is directed-sups-preserving by Th46; :: thesis: verum
end;
assume inf_op L is directed-sups-preserving ; :: thesis: L is meet-continuous
then for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th43;
hence ( L is up-complete & L is satisfying_MC ) by Th44; :: according to WAYBEL_2:def 7 :: thesis: verum