let L be non empty Boolean RelStr ; :: thesis: for a, b, c being Element of L holds (a \ b) \ c = a \ (b "\/" c)
let a, b, c be Element of L; :: thesis: (a \ b) \ c = a \ (b "\/" c)
thus (a \ b) \ c = a "/\" (('not' b) "/\" ('not' c)) by LATTICE3:16
.= a \ (b "\/" c) by Th36 ; :: thesis: verum