let L be complete Semilattice; :: thesis: ( L is meet-continuous iff for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" () = sup (x "/\" ()) )

hereby :: thesis: ( ( for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" () = sup (x "/\" ()) ) implies L is meet-continuous )
assume L is meet-continuous ; :: thesis: for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" () = sup (x "/\" ())

then 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 Th54;
hence for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" () = sup (x "/\" ()) by Th47; :: thesis: verum
end;
assume for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" () = sup (x "/\" ()) ; :: thesis:
then 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 Th48;
hence ( L is up-complete & L is satisfying_MC ) by Th42; :: according to WAYBEL_2:def 7 :: thesis: verum