let L be lower-bounded Semilattice; :: thesis: for a being Element of L holds (Bottom L) \ a = Bottom L
let a be Element of L; :: thesis: (Bottom L) \ a = Bottom L
thus (Bottom L) \ a = (Bottom L) "/\" ('not' a)
.= Bottom L by Th10, YELLOW_0:44 ; :: thesis: verum