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 )

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_{1} being set

for b_{2} being set

for b_{3} being ManySortedFunction of b_{2},b_{1} --> the carrier of L holds //\ ((\// (b_{3},L)),L) = \\/ ((/\\ ((Frege b_{3}),L)),L)

let J be non empty set ; :: thesis: for b_{1} being set

for b_{2} being ManySortedFunction of b_{1},J --> the carrier of L holds //\ ((\// (b_{2},L)),L) = \\/ ((/\\ ((Frege b_{2}),L)),L)

let K be V8() ManySortedSet of J; :: thesis: for b_{1} being ManySortedFunction of K,J --> the carrier of L holds //\ ((\// (b_{1},L)),L) = \\/ ((/\\ ((Frege b_{1}),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

thus ( L is completely-distributive implies L opp is completely-distributive ) :: thesis: ( L opp is completely-distributive implies L is completely-distributive )

proof

assume A2:
L opp is completely-distributive
; :: thesis: L is completely-distributive
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_{1} being set

for b_{2} being set

for b_{3} being ManySortedFunction of b_{2},b_{1} --> the carrier of (L opp) holds //\ ((\// (b_{3},(L opp))),(L opp)) = \\/ ((/\\ ((Frege b_{3}),(L opp))),(L opp))

let J be non empty set ; :: thesis: for b_{1} being set

for b_{2} being ManySortedFunction of b_{1},J --> the carrier of (L opp) holds //\ ((\// (b_{2},(L opp))),(L opp)) = \\/ ((/\\ ((Frege b_{2}),(L opp))),(L opp))

let K be V8() ManySortedSet of J; :: thesis: for b_{1} being ManySortedFunction of K,J --> the carrier of (L opp) holds //\ ((\// (b_{1},(L opp))),(L opp)) = \\/ ((/\\ ((Frege b_{1}),(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;hence L opp is complete ; :: according to WAYBEL_5:def 3 :: thesis: for b

for b

for b

let J be non empty set ; :: thesis: for b

for b

let K be V8() ManySortedSet of J; :: thesis: for b

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

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

for b

for b

let J be non empty set ; :: thesis: for b

for b

let K be V8() ManySortedSet of J; :: thesis: for b

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