theorem ThC: :: LATSTONE:3

for L being Lattice
for I being non empty ClosedSubset of L st L is upper-bounded & Top L in I holds
( latt (L,I) is upper-bounded & Top (latt (L,I)) = Top L )