let X be non empty TopSpace; for X0 being SubSpace of X holds
( X0 is open SubSpace of X iff modid (X,X0) is continuous Function of X,(X modified_with_respect_to X0) )
let X0 be SubSpace of X; ( X0 is open SubSpace of X iff modid (X,X0) is continuous Function of X,(X modified_with_respect_to X0) )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
thus
( X0 is open SubSpace of X implies modid (X,X0) is continuous Function of X,(X modified_with_respect_to X0) )
( modid (X,X0) is continuous Function of X,(X modified_with_respect_to X0) implies X0 is open SubSpace of X )
thus
( modid (X,X0) is continuous Function of X,(X modified_with_respect_to X0) implies X0 is open SubSpace of X )
verum