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