theorem Th48: :: YELLOW_7:48
for L being complete LATTICE holds
( L is completely-distributive iff for J being non empty set
for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup = Inf )