theorem Th51: :: LATTICE2:51

for L being 0_Lattice holds Bottom L is_a_unity_wrt the L_join of L