:: deftheorem defines -extension_of_the_topology_of TMAP_1:def 7 :
for X being non empty TopSpace
for A being Subset of X holds A -extension_of_the_topology_of X = { (H \/ (G /\ A)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } ;