let L be GAD_Lattice; :: thesis: ( L is trivial implies L is with_zero )
assume L is trivial ; :: thesis: L is with_zero
then reconsider LL = L as trivial GAD_Lattice ;
set a = the Element of LL;
for x being Element of LL holds the Element of LL "/\" x = the Element of LL by SUBSET_1:def 7;
hence L is with_zero ; :: thesis: verum