let X be non empty TopSpace; :: thesis: for D being Subset of X
for C being Subset of (X modified_with_respect_to (D `)) st C = D holds
C is closed
let D be Subset of X; :: thesis: for C being Subset of (X modified_with_respect_to (D `)) st C = D holds
C is closed
let C be Subset of (X modified_with_respect_to (D `)); :: thesis: ( C = D implies C is closed )
assume C = D ; :: thesis: C is closed
then C ` = D ` by TMAP_1:93;
then C ` is open by TMAP_1:94;
hence C is closed ; :: thesis: verum