for X being non empty TopSpace
for A being Subset of X holds the topology of X c= A -extension_of_the_topology_of X