theorem :: YELLOW_1:24

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