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