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 )
assume A1: X [= Bottom L ; :: thesis: X = Bottom L
Bottom L [= X by LATTICES:41;
hence X = Bottom L by A1, LATTICES:26; :: thesis: verum