let L be non empty Poset; :: thesis:
thus ( L is completely-distributive implies L opp is completely-distributive ) :: thesis: ( L opp is completely-distributive implies L is completely-distributive )
proof
assume A1: L is completely-distributive ; :: thesis:
hence L opp is complete ; :: according to WAYBEL_5:def 3 :: thesis: for b1 being set
for b2 being set
for b3 being ManySortedFunction of b2,b1 --> the carrier of (L opp) holds //\ ((\// (b3,(L opp))),(L opp)) = \\/ ((/\\ ((Frege b3),(L opp))),(L opp))

let J be non empty set ; :: thesis: for b1 being set
for b2 being ManySortedFunction of b1,J --> the carrier of (L opp) holds //\ ((\// (b2,(L opp))),(L opp)) = \\/ ((/\\ ((Frege b2),(L opp))),(L opp))

let K be V8() ManySortedSet of J; :: thesis: for b1 being ManySortedFunction of K,J --> the carrier of (L opp) holds //\ ((\// (b1,(L opp))),(L opp)) = \\/ ((/\\ ((Frege b1),(L opp))),(L opp))
let F be DoubleIndexedSet of K,(L opp); :: thesis: //\ ((\// (F,(L opp))),(L opp)) = \\/ ((/\\ ((),(L opp))),(L opp))
reconsider G = F as DoubleIndexedSet of K,L ;
thus Inf = \\/ ((),L) by
.= Sup by
.= Inf by
.= //\ ((),L) by
.= Sup by ; :: thesis: verum
end;
assume A2: L opp is completely-distributive ; :: thesis:
then A3: L is non empty complete Poset by Th17;
thus L is complete by ; :: according to WAYBEL_5:def 3 :: thesis: for b1 being set
for b2 being set
for b3 being ManySortedFunction of b2,b1 --> the carrier of L holds //\ ((\// (b3,L)),L) = \\/ ((/\\ ((Frege b3),L)),L)

let J be non empty set ; :: thesis: for b1 being set
for b2 being ManySortedFunction of b1,J --> the carrier of L holds //\ ((\// (b2,L)),L) = \\/ ((/\\ ((Frege b2),L)),L)

let K be V8() ManySortedSet of J; :: thesis: for b1 being ManySortedFunction of K,J --> the carrier of L holds //\ ((\// (b1,L)),L) = \\/ ((/\\ ((Frege b1),L)),L)
let F be DoubleIndexedSet of K,L; :: thesis: //\ ((\// (F,L)),L) = \\/ ((/\\ ((),L)),L)
reconsider G = F as DoubleIndexedSet of K,(L opp) ;
thus Inf = \\/ ((),(L opp)) by
.= Sup by
.= Inf by
.= //\ ((),(L opp)) by
.= Sup by ; :: thesis: verum