let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X holds

( the carrier of (X modified_with_respect_to X0) = the carrier of X & ( for A being Subset of X st A = the carrier of X0 holds

the topology of (X modified_with_respect_to X0) = A -extension_of_the_topology_of X ) )

let X0 be non empty SubSpace of X; :: thesis: ( the carrier of (X modified_with_respect_to X0) = the carrier of X & ( for A being Subset of X st A = the carrier of X0 holds

the topology of (X modified_with_respect_to X0) = A -extension_of_the_topology_of X ) )

set Y = X modified_with_respect_to X0;

reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;

A1: X modified_with_respect_to X0 = X modified_with_respect_to A by Def10;

hence the carrier of (X modified_with_respect_to X0) = the carrier of X ; :: thesis: for A being Subset of X st A = the carrier of X0 holds

the topology of (X modified_with_respect_to X0) = A -extension_of_the_topology_of X

thus for A being Subset of X st A = the carrier of X0 holds

the topology of (X modified_with_respect_to X0) = A -extension_of_the_topology_of X by A1; :: thesis: verum

( the carrier of (X modified_with_respect_to X0) = the carrier of X & ( for A being Subset of X st A = the carrier of X0 holds

the topology of (X modified_with_respect_to X0) = A -extension_of_the_topology_of X ) )

let X0 be non empty SubSpace of X; :: thesis: ( the carrier of (X modified_with_respect_to X0) = the carrier of X & ( for A being Subset of X st A = the carrier of X0 holds

the topology of (X modified_with_respect_to X0) = A -extension_of_the_topology_of X ) )

set Y = X modified_with_respect_to X0;

reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;

A1: X modified_with_respect_to X0 = X modified_with_respect_to A by Def10;

hence the carrier of (X modified_with_respect_to X0) = the carrier of X ; :: thesis: for A being Subset of X st A = the carrier of X0 holds

the topology of (X modified_with_respect_to X0) = A -extension_of_the_topology_of X

thus for A being Subset of X st A = the carrier of X0 holds

the topology of (X modified_with_respect_to X0) = A -extension_of_the_topology_of X by A1; :: thesis: verum