let X be non empty TopSpace; :: thesis: for A being Subset of X holds A in A -extension_of_the_topology_of X
let A be Subset of X; :: thesis: A in A -extension_of_the_topology_of X
X is SubSpace of X by TSEP_1:2;
then reconsider G = the carrier of X as Subset of X by TSEP_1:1;
A1: G in the topology of X by PRE_TOPC:def 1;
{} X = {} ;
then reconsider H = {} as Subset of X ;
( A = H \/ (G /\ A) & H in the topology of X ) by PRE_TOPC:1, XBOOLE_1:28;
hence A in A -extension_of_the_topology_of X by A1; :: thesis: verum