let L be 1 -element Poset; :: thesis: L is completely-distributive
reconsider L9 = L as complete LATTICE ;
thus L is complete ; :: according to WAYBEL_5:def 3 :: thesis: for J being non empty set
for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf = Sup
reconsider L9 = L9 as continuous LATTICE ;
for J being non empty set
for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L9 holds Inf = Sup

proof

let J be non empty set ; :: thesis: for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L9 holds Inf = Sup
let K be non-empty ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,L9 holds Inf = Sup
let F be DoubleIndexedSet of K,L9; :: thesis: Inf = Sup
for j being Element of J holds rng (F . j) is directed ;
hence Inf = Sup by Lm8; :: thesis: verum

end;

hence for J being non empty set
for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf = Sup ; :: thesis: verum