for L being complete LATTICE
for J being non empty set
for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf >= Sup