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