theorem Th18: :: LATTICE2:18

for L being Lattice st the L_join of L is having_a_unity holds
Bottom L = the_unity_wrt the L_join of L