let L be non empty Poset; :: thesis: ( L is trivial implies L is completely-distributive )
assume A1: L is trivial ; :: thesis: L is completely-distributive
then reconsider L9 = L as complete LATTICE ;
thus L is complete by A1; :: 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 by A1;
for J being non empty set
for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L9 holds Inf = Sup

proof

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

proof

let j be Element of J; :: thesis: rng (F . j) is directed
for x, y being Element of L st x in rng (F . j) & y in rng (F . j) holds
ex z being Element of L st
( z in rng (F . j) & x <= z & y <= z )

proof

consider z being Element of rng (F . j);
let x, y be Element of L; :: thesis: ( x in rng (F . j) & y in rng (F . j) implies ex z being Element of L st
( z in rng (F . j) & x <= z & y <= z ) )
assume that
x in rng (F . j) and
y in rng (F . j) ; :: thesis: ex z being Element of L st
( z in rng (F . j) & x <= z & y <= z )
reconsider z = z as Element of L ;
take z ; :: thesis: ( z in rng (F . j) & x <= z & y <= z )
thus ( z in rng (F . j) & x <= z & y <= z ) by A1, STRUCT_0:def 10; :: thesis: verum

end;

hence rng (F . j) is directed by WAYBEL_0:def 1; :: thesis: verum

end;

hence Inf = Sup by Lm8; :: thesis: verum

end;

hence for J being non empty set
for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf = Sup ; :: thesis: verum
consider x being Element of L;