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 "\/" c) = a "/\" (('not' b) "/\" ('not' c)) by Th36
.= (a "/\" a) "/\" (('not' b) "/\" ('not' c)) by Th2
.= ((a "/\" a) "/\" ('not' b)) "/\" ('not' c) by LATTICE3:16
.= (a "/\" (a "/\" ('not' b))) "/\" ('not' c) by LATTICE3:16
.= (a \ b) "/\" (a \ c) by LATTICE3:16 ; :: thesis: verum