for L being complete LATTICE st ( for J being non empty set st J in the_universe_of the carrier of L holds
for K being V9() ManySortedSet of J st ( for j being Element of J holds K . j in the_universe_of the carrier of L ) holds
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup ) holds
L is continuous