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 )

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

( 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

A2:
[#] (X modified_with_respect_to A) <> {}
;
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;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

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