let L be 0_Lattice; :: thesis: for a being Element of L holds Bottom L [= a
let a be Element of L; :: thesis: Bottom L [= a
Bottom L [= (Bottom L) "\/" a by Th22;
hence Bottom L [= a by Th39; :: thesis: verum