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