let L be with_zero GAD_Lattice; :: thesis: for x being Element of L holds x "\/" (bottom L) = x
let x be Element of L; :: thesis: x "\/" (bottom L) = x
(bottom L) "/\" x = bottom L by GADL0;
then a1: bottom L [= x by LATTICES:def 8;
set b1 = bottom L;
x "/\" (bottom L) = x "/\" ((bottom L) "/\" x) by GADL0
.= (x "/\" (bottom L)) "/\" x by LATTICES:def 7
.= ((bottom L) "/\" x) "/\" x by Lem310
.= (bottom L) "/\" x by GADL0 ;
then ((bottom L) "/\" x) "\/" (bottom L) = bottom L by LATTICES:def 8;
hence x "\/" (bottom L) = x by a1, Th3716; :: thesis: verum