let X be non empty TopSpace; :: thesis: for A being Subset of X holds
( A is open iff modid X,A is continuous Function of X,(X modified_with_respect_to A) )
let A be Subset of X; :: thesis: ( A is open iff modid X,A is continuous Function of X,(X modified_with_respect_to A) )
A1: [#] (X modified_with_respect_to A) <> {} ;
thus ( A is open implies modid X,A is continuous Function of X,(X modified_with_respect_to A) ) :: thesis: ( modid X,A is continuous Function of X,(X modified_with_respect_to A) implies A is open )

proof

assume A is open ; :: thesis: modid X,A is continuous Function of X,(X modified_with_respect_to A)
then A2: TopStruct(# the carrier of X,the topology of X #) = X modified_with_respect_to A by Th106;
reconsider f = modid X,A as Function of X,X ;
f = id X ;
then f is continuous Function of X,X by Th94;
hence modid X,A is continuous Function of X,(X modified_with_respect_to A) by A2, Th56; :: thesis: verum

end;

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

proof

assume A3: modid X,A is continuous Function of X,(X modified_with_respect_to A) ; :: thesis: A is open
set B = (modid X,A) .: A;
A4: (modid X,A) .: A = A by FUNCT_1:162;
A5: (modid X,A) .: A is open by Th105, FUNCT_1:162;
(modid X,A) " ((modid X,A) .: A) = A by A4, FUNCT_2:171;
hence A is open by A1, A3, A5, TOPS_2:55; :: thesis: verum

end;