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

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