take L = the trivial GAD_Lattice; :: thesis: L is with_zero
thus L is with_zero ; :: thesis: verum