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, Th101; :: 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, Th101;
hence X0 is open SubSpace of X by TSEP_1:16; :: thesis: verum
end;