theorem :: HEYTING3:6

for L being upper-bounded Lattice holds Top L = Top (LattPOSet L)