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 L is completely-distributive ; :: thesis: L opp is completely-distributive
then A1: L is non empty completely-distributive Poset ;
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 V5() ManySortedSet of ; :: 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 L opp is completely-distributive ; :: thesis: L is completely-distributive
then A2: L opp is non empty completely-distributive Poset ;
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 V5() ManySortedSet of ; :: 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