let L be 0_Lattice; :: thesis: for a being Element of L holds (Bottom L) "\/" a = a
let a be Element of L; :: thesis: (Bottom L) "\/" a = a
thus (Bottom L) "\/" a = ((Bottom L) "/\" a) "\/" a by Def16
.= a by Def8 ; :: thesis: verum