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) )
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

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

end;

A2: [#] (X modified_with_respect_to A) <> {} ;
thus ( modid X,A is continuous Function of X,(X modified_with_respect_to A) implies A is open ) :: thesis: verum

proof

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

end;