let L be LATTICE; :: thesis: ( L is distributive iff L opp is distributive )

hereby :: thesis: ( L opp is distributive implies L is distributive )

assume A1: L is distributive ; :: thesis: L opp is distributive
thus L opp is distributive :: thesis: verum

proof

let x, y, z be Element of (L opp ); :: according to WAYBEL_1:def 3 :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
thus x "/\" (y "\/" z) = (~ x) "\/" (~ (y "\/" z)) by Th24
.= (~ x) "\/" ((~ y) "/\" (~ z)) by Th22
.= ((~ x) "\/" (~ y)) "/\" ((~ x) "\/" (~ z)) by A1, WAYBEL_1:6
.= (~ (x "/\" y)) "/\" ((~ x) "\/" (~ z)) by Th24
.= (~ (x "/\" y)) "/\" (~ (x "/\" z)) by Th24
.= (x "/\" y) "\/" (x "/\" z) by Th22 ; :: thesis: verum

end;

end;

assume A2: L opp is distributive ; :: thesis: L is distributive
let x, y, z be Element of L; :: according to WAYBEL_1:def 3 :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
thus x "/\" (y "\/" z) = (x ~ ) "\/" ((y "\/" z) ~ ) by Th21
.= (x ~ ) "\/" ((y ~ ) "/\" (z ~ )) by Th23
.= ((x ~ ) "\/" (y ~ )) "/\" ((x ~ ) "\/" (z ~ )) by A2, WAYBEL_1:6
.= ((x "/\" y) ~ ) "/\" ((x ~ ) "\/" (z ~ )) by Th21
.= ((x "/\" y) ~ ) "/\" ((x "/\" z) ~ ) by Th21
.= (x "/\" y) "\/" (x "/\" z) by Th23 ; :: thesis: verum