theorem Th56: :: LATTICE2:56

for L being 1_Lattice holds Top L is_a_unity_wrt the L_meet of L