theorem Th16: :: WAYBEL_5:16

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 holds Inf >= Sup