let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X
for Y0 being SubSpace of X modified_with_respect_to X0 st the carrier of Y0 = the carrier of X0 holds
Y0 is open SubSpace of X modified_with_respect_to X0
let X0 be non empty SubSpace of X; :: thesis: for Y0 being SubSpace of X modified_with_respect_to X0 st the carrier of Y0 = the carrier of X0 holds
Y0 is open SubSpace of X modified_with_respect_to X0
let Y0 be SubSpace of X modified_with_respect_to X0; :: thesis: ( the carrier of Y0 = the carrier of X0 implies Y0 is open SubSpace of X modified_with_respect_to X0 )
assume A1: the carrier of Y0 = the carrier of X0 ; :: thesis: Y0 is open SubSpace of X modified_with_respect_to X0
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
set Y = X modified_with_respect_to X0;
reconsider B = the carrier of Y0 as Subset of (X modified_with_respect_to X0) by TSEP_1:1;
X modified_with_respect_to X0 = X modified_with_respect_to A by Def10;
then B is open by A1, Th94;
hence Y0 is open SubSpace of X modified_with_respect_to X0 by TSEP_1:16; :: thesis: verum