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 ) = sup (x "/\" (FinSups f)) )

for J being set

for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ; :: thesis: L is meet-continuous

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

for J being set

for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) )

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 ) = sup (x "/\" (FinSups f)) ) implies L is meet-continuous )

assume
for x being Element of Lfor J being set

for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ) 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 ) = sup (x "/\" (FinSups f))

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 ) = sup (x "/\" (FinSups f)) by Th47; :: thesis: verum

end;for J being set

for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f))

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 ) = sup (x "/\" (FinSups f)) by Th47; :: thesis: verum

for J being set

for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ; :: thesis: L is meet-continuous

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