let L be Lattice; :: thesis: ( ( for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) ) iff for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) )

hereby :: thesis: ( ( for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) ) implies for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) )

assume A1: for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) ; :: thesis: for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)
let a, b, c be Element of L; :: thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)
thus a "\/" (b "/\" c) = (a "\/" (c "/\" a)) "\/" (c "/\" b) by Def8
.= a "\/" ((c "/\" a) "\/" (c "/\" b)) by Def5
.= a "\/" ((a "\/" b) "/\" c) by A1
.= ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" c) by Def9
.= (a "\/" b) "/\" (a "\/" c) by A1 ; :: thesis: verum

end;

assume A2: for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) ; :: thesis: for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
let a, b, c be Element of L; :: thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
thus a "/\" (b "\/" c) = (a "/\" (c "\/" a)) "/\" (c "\/" b) by Def9
.= a "/\" ((c "\/" a) "/\" (c "\/" b)) by Def7
.= a "/\" ((a "/\" b) "\/" c) by A2
.= ((a "/\" b) "\/" a) "/\" ((a "/\" b) "\/" c) by Def8
.= (a "/\" b) "\/" (a "/\" c) by A2 ; :: thesis: verum