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