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