let L be with_zero GAD_Lattice; :: thesis: for x being Element of L holds (bottom L) "\/" x = x
let x be Element of L; :: thesis: (bottom L) "\/" x = x
(bottom L) "/\" x = bottom L by GADL0;
hence (bottom L) "\/" x = x by LATTICES:def 8; :: thesis: verum