for L being complete LATTICE holds
( L is continuous iff for J, K being non empty set
for F being Function of [:J,K:], the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds
Inf = Sup ) by Lm8, Lm10;