theorem Th9: :: OPENLATT:9

for T being non empty TopSpace holds Top (Open_setLatt T) = the carrier of T