let L be LATTICE; :: thesis: ( L is distributive iff for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) )
hereby :: thesis: ( ( for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) ) implies L is distributive )
assume A1: L is distributive ; :: thesis: for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z)
let x, y, z be Element of L; :: thesis: x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z)
thus x "\/" (y "/\" z) = (x "\/" (z "/\" x)) "\/" (y "/\" z) by LATTICE3:17
.= x "\/" ((z "/\" x) "\/" (z "/\" y)) by LATTICE3:14
.= x "\/" ((x "\/" y) "/\" z) by A1
.= ((x "\/" y) "/\" x) "\/" ((x "\/" y) "/\" z) by LATTICE3:18
.= (x "\/" y) "/\" (x "\/" z) by A1 ; :: thesis: verum
end;
assume A2: for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) ; :: 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 "/\" (x "\/" z)) "/\" (y "\/" z) by LATTICE3:18
.= x "/\" ((z "\/" x) "/\" (y "\/" z)) by LATTICE3:16
.= x "/\" (z "\/" (x "/\" y)) by A2
.= ((y "/\" x) "\/" x) "/\" ((x "/\" y) "\/" z) by LATTICE3:17
.= (x "/\" y) "\/" (x "/\" z) by A2 ; :: thesis: verum