theorem Th57: :: FILTER_0:57

for L being Lattice
for p being Element of L st L is upper-bounded holds
Top (latt <.p.)) = Top L