let X be non empty TopSpace; :: thesis: 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; :: thesis: ( 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) ) :: thesis: ( modid X,X0 is continuous Function of X,(X modified_with_respect_to X0) implies X0 is open SubSpace of X )

proof

assume X0 is open SubSpace of X ; :: thesis: modid X,X0 is continuous Function of X,(X modified_with_respect_to X0)
then A1: A is open by TSEP_1:16;
( X modified_with_respect_to X0 = X modified_with_respect_to A & modid X,X0 = modid X,A ) by Def10, Def11;
hence modid X,X0 is continuous Function of X,(X modified_with_respect_to X0) by A1, Th113; :: thesis: verum

end;

thus ( modid X,X0 is continuous Function of X,(X modified_with_respect_to X0) implies X0 is open SubSpace of X ) :: thesis: verum

proof

assume A2: modid X,X0 is continuous Function of X,(X modified_with_respect_to X0) ; :: thesis: X0 is open SubSpace of X
( X modified_with_respect_to X0 = X modified_with_respect_to A & modid X,X0 = modid X,A ) by Def10, Def11;
then A is open by A2, Th113;
hence X0 is open SubSpace of X by TSEP_1:16; :: thesis: verum

end;