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 Th5;
hence Bottom L [= a ; :: thesis: verum