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

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