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 )
A1: X "/\" (Y "/\" (X `)) = Y "/\" ((X `) "/\" X) by LATTICES:def 7
.= Y "/\" (Bottom L) by LATTICES:20
.= Bottom L ;
assume X [= Y \ X ; :: thesis: X = Bottom L
hence X = Bottom L by A1, LATTICES:4; :: thesis: verum