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 )

( 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

thus
( modid (X,X0) is continuous Function of X,(X modified_with_respect_to X0) implies X0 is open SubSpace of X )
:: thesis: verum
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, Th101; :: thesis: verum

end;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, Th101; :: 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, Th101;

hence X0 is open SubSpace of X by TSEP_1:16; :: thesis: verum

end;( 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, Th101;

hence X0 is open SubSpace of X by TSEP_1:16; :: thesis: verum