for L being up-complete Semilattice holds
( L is meet-continuous iff for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) by Th41, Th42;