:: deftheorem defines modified_with_respect_to TMAP_1:def 8 :
for X being non empty TopSpace
for A being Subset of X holds X modified_with_respect_to A = TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #);