let L be non empty Boolean RelStr ; :: 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)
((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" (b "/\" c)) "/\" (b "\/" (b "/\" c))) "\/" (c "/\" a) by WAYBEL_1:5
.= ((a "\/" (b "/\" c)) "/\" b) "\/" (c "/\" a) by LATTICE3:17
.= ((a "\/" (b "/\" c)) "\/" (c "/\" a)) "/\" (b "\/" (c "/\" a)) by WAYBEL_1:5
.= ((a "\/" (b "/\" c)) "\/" (c "/\" a)) "/\" ((b "\/" c) "/\" (b "\/" a)) by WAYBEL_1:5
.= ((b "/\" c) "\/" (a "\/" (c "/\" a))) "/\" ((b "\/" c) "/\" (b "\/" a)) by LATTICE3:14
.= ((b "/\" c) "\/" a) "/\" ((b "\/" c) "/\" (b "\/" a)) by LATTICE3:17
.= ((b "\/" a) "/\" (c "\/" a)) "/\" ((b "\/" c) "/\" (b "\/" a)) by WAYBEL_1:5
.= (b "\/" a) "/\" (((c "\/" a) "/\" (b "\/" a)) "/\" (b "\/" c)) by LATTICE3:16
.= (b "\/" a) "/\" ((b "\/" a) "/\" ((c "\/" a) "/\" (b "\/" c))) by LATTICE3:16
.= ((b "\/" a) "/\" (b "\/" a)) "/\" ((c "\/" a) "/\" (b "\/" c)) by LATTICE3:16
.= (b "\/" a) "/\" ((c "\/" a) "/\" (b "\/" c)) by Th2
.= ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) by LATTICE3:16 ;
hence ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) ; :: thesis: verum