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 V9() 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 V9() ManySortedSet of J

for F being DoubleIndexedSet of K,L9 holds Inf = Sup

for K being V9() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Inf = Sup ; :: thesis: verum

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 V9() 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 V9() ManySortedSet of J

for F being DoubleIndexedSet of K,L9 holds Inf = Sup

proof

hence
for J being non empty set
let J be non empty set ; :: thesis: for K being V9() ManySortedSet of J

for F being DoubleIndexedSet of K,L9 holds Inf = Sup

let K be V9() 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;for F being DoubleIndexedSet of K,L9 holds Inf = Sup

let K be V9() 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

for K being V9() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Inf = Sup ; :: thesis: verum