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

let A be Subset of X; :: thesis: ( A is open iff modid (X,A) is continuous Function of X,() )
thus ( A is open implies modid (X,A) is continuous Function of X,() ) :: thesis: ( modid (X,A) is continuous Function of X,() 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,()
then TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to A by Th95;
hence modid (X,A) is continuous Function of X,() by ; :: thesis: verum
end;
A2: [#] () <> {} ;
thus ( modid (X,A) is continuous Function of X,() implies A is open ) :: thesis: verum
proof
set B = (modid (X,A)) .: A;
assume A3: modid (X,A) is continuous Function of X,() ; :: thesis: A is open
(modid (X,A)) .: A = A by FUNCT_1:92;
then A4: (modid (X,A)) " ((modid (X,A)) .: A) = A by FUNCT_2:94;
(modid (X,A)) .: A is open by ;
hence A is open by ; :: thesis: verum
end;