theorem :: WAYBEL_5:19

for L being complete LATTICE holds
( L is continuous iff for J being non empty set
for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup ) by Lm8, Lm9;