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 Th95;
hence modid (X,A) is continuous Function of X,(X modified_with_respect_to A) by A1, Th51; :: 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:92;
then A4: (modid (X,A)) " ((modid (X,A)) .: A) = A by FUNCT_2:94;
(modid (X,A)) .: A is open by Th94, FUNCT_1:92;
hence A is open by A2, A3, A4, TOPS_2:43; :: thesis: verum
end;