theorem :: LATTICE2:62

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