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

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