let L be up-complete Semilattice; :: thesis: ( L is meet-continuous iff for x being Element of L
for N being non empty prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap N,L))) )
thus ( L is meet-continuous implies for x being Element of L
for N being non empty prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap N,L))) ) by Th41; :: thesis: ( ( for x being Element of L
for N being non empty prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap N,L))) ) implies L is meet-continuous )
assume for x being Element of L
for N being non empty prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap N,L))) ; :: thesis: L is meet-continuous
hence ( L is up-complete & L is satisfying_MC ) by Th42; :: according to WAYBEL_2:def 7 :: thesis: verum