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:5
.= (~ (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:5
.= ((x "/\" y) ~) "/\" ((x ~) "\/" (z ~)) by Th21
.= ((x "/\" y) ~) "/\" ((x "/\" z) ~) by Th21
.= (x "/\" y) "\/" (x "/\" z) by Th23 ; :: thesis: verum