theorem Th27: :: WAYBEL_5:27

for L being complete LATTICE
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
rng (Infs ) is directed