theorem Th41: :: FILTER_2:41

for L being Lattice
for D being non empty Subset of L st L is upper-bounded & Top L in D holds
( (.D.> = (.L.> & (.D.> = the carrier of L )