let L be up-complete Semilattice; :: thesis: ( L is meet-continuous iff inf_op L is directed-sups-preserving )

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

hereby :: thesis: ( inf_op L is directed-sups-preserving implies L is meet-continuous )

assume
inf_op L is directed-sups-preserving
; :: thesis: 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;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

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