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