theorem Th58: :: FILTER_0:58
for L being Lattice
for p being Element of L st L is 1_Lattice holds
latt <.p.) is bounded by Th52;