theorem :: WAYBEL_2:55

for L being complete Semilattice holds
( 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)) )