let L be 0_Lattice; :: thesis: for X being Element of L st X [= Bottom L holds
X = Bottom L
let X be Element of L; :: thesis: ( X [= Bottom L implies X = Bottom L )
A1: Bottom L [= X by LATTICES:16;
assume X [= Bottom L ; :: thesis: X = Bottom L
hence X = Bottom L by A1, LATTICES:8; :: thesis: verum