let L be non empty Boolean RelStr ; :: 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) \ (a "/\" c) = (a "/\" b) "/\" (('not' a) "\/" ('not' c)) by Th36
.= ((a "/\" b) "/\" ('not' a)) "\/" ((a "/\" b) "/\" ('not' c)) by WAYBEL_1:def 3
.= ((a "/\" ('not' a)) "/\" b) "\/" ((a "/\" b) "/\" ('not' c)) by LATTICE3:16
.= ((Bottom L) "/\" b) "\/" ((a "/\" b) "/\" ('not' c)) by Th34
.= (Bottom L) "\/" ((a "/\" b) "/\" ('not' c)) by WAYBEL_1:3
.= (a "/\" b) "/\" ('not' c) by WAYBEL_1:3
.= a "/\" (b \ c) by LATTICE3:16 ; :: thesis: verum