theorem :: LATTICE2:61

for L being 0_Lattice holds Bottom L = Top (L .:)