let L be B_Lattice; :: thesis: for X, Y being Element of L st X [= Y \ X holds
X = Bottom L
let X, Y be Element of L; :: thesis: ( X [= Y \ X implies X = Bottom L )
assume A1: X [= Y \ X ; :: thesis: X = Bottom L
X "/\" (Y "/\" (X ` )) = Y "/\" ((X ` ) "/\" X) by LATTICES:def 7
.= Y "/\" (Bottom L) by LATTICES:47
.= Bottom L by LATTICES:40 ;
hence X = Bottom L by A1, LATTICES:21; :: thesis: verum