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
consider x being Element of L;
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
for F being DoubleIndexedSet of K,L holds Inf = Sup
then L is non empty complete Poset ;
then reconsider L' = L as complete LATTICE ;
for x being Element of L' holds x = sup (waybelow x) by A1, STRUCT_0:def 10;
then A2: L' is satisfying_axiom_of_approximation by WAYBEL_3:def 5;
reconsider L' = L' as continuous LATTICE by A2;
for J being non empty set
for K being V9() ManySortedSet of
for F being DoubleIndexedSet of K,L' holds Inf = Sup

proof

let J be non empty set ; :: thesis: for K being V9() ManySortedSet of
for F being DoubleIndexedSet of K,L' holds Inf = Sup
let K be V9() ManySortedSet of ; :: thesis: for F being DoubleIndexedSet of K,L' holds Inf = Sup
let F be DoubleIndexedSet of K,L'; :: 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

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 ( x in rng (F . j) & y in rng (F . j) ) ; :: thesis: ex z being Element of L st
( z in rng (F . j) & x <= z & y <= z )
consider z being Element of rng (F . j);
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
for F being DoubleIndexedSet of K,L holds Inf = Sup ; :: thesis: verum