let L be non empty Poset; :: thesis: ( L is completely-distributive iff L opp is completely-distributive )
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: L opp is completely-distributive
hence L opp is complete ; :: according to WAYBEL_5:def 3 :: thesis: for b₁ being set
for b₂ being set
for b₃ being ManySortedFunction of b₂,b₁ --> the carrier of (L opp) holds //\ ((\// (b₃,(L opp))),(L opp)) = \\/ ((/\\ ((Frege b₃),(L opp))),(L opp))
let J be non empty set ; :: thesis: for b₁ being set
for b₂ being ManySortedFunction of b₁,J --> the carrier of (L opp) holds //\ ((\// (b₂,(L opp))),(L opp)) = \\/ ((/\\ ((Frege b₂),(L opp))),(L opp))
let K be non-empty ManySortedSet of J; :: thesis: for b₁ being ManySortedFunction of K,J --> the carrier of (L opp) holds //\ ((\// (b₁,(L opp))),(L opp)) = \\/ ((/\\ ((Frege b₁),(L opp))),(L opp))
let F be DoubleIndexedSet of K,(L opp); :: thesis: //\ ((\// (F,(L opp))),(L opp)) = \\/ ((/\\ ((Frege F),(L opp))),(L opp))
reconsider G = F as DoubleIndexedSet of K,L ;
thus Inf = \\/ ((Sups ),L) by A1, Th49
.= Sup by A1, Th50
.= Inf by A1, Th48
.= //\ ((Infs ),L) by A1, Th50
.= Sup by A1, Th49 ; :: thesis: verum

end;

assume A2: L opp is completely-distributive ; :: thesis: L is completely-distributive
then A3: L is non empty complete Poset by Th17;
thus L is complete by A2, Th17; :: according to WAYBEL_5:def 3 :: thesis: for b₁ being set
for b₂ being set
for b₃ being ManySortedFunction of b₂,b₁ --> the carrier of L holds //\ ((\// (b₃,L)),L) = \\/ ((/\\ ((Frege b₃),L)),L)
let J be non empty set ; :: thesis: for b₁ being set
for b₂ being ManySortedFunction of b₁,J --> the carrier of L holds //\ ((\// (b₂,L)),L) = \\/ ((/\\ ((Frege b₂),L)),L)
let K be non-empty ManySortedSet of J; :: thesis: for b₁ being ManySortedFunction of K,J --> the carrier of L holds //\ ((\// (b₁,L)),L) = \\/ ((/\\ ((Frege b₁),L)),L)
let F be DoubleIndexedSet of K,L; :: thesis: //\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L)
reconsider G = F as DoubleIndexedSet of K,(L opp) ;
thus Inf = \\/ ((Sups ),(L opp)) by A3, Th49
.= Sup by A3, Th50
.= Inf by A2, Th48
.= //\ ((Infs ),(L opp)) by A3, Th50
.= Sup by A3, Th49 ; :: thesis: verum