theorem :: LATTICE2:52

for L being 0_Lattice holds Bottom L = the_unity_wrt the L_join of L by Th18;