let X be non empty TopSpace; :: thesis: for A being Subset of holds A in A -extension_of_the_topology_of X
let A be Subset of ; :: 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 by TSEP_1:1;
A1: G in the topology of X by PRE_TOPC:def 1;
{} X = {} ;
then reconsider H = {} as Subset of ;
( A = H \/ (G /\ A) & H in the topology of X ) by PRE_TOPC:5, XBOOLE_1:28;
hence A in A -extension_of_the_topology_of X by A1; :: thesis: verum