let X be non empty TopSpace; :: thesis: for D, B being Subset of X
for C being Subset of (X modified_with_respect_to D) st B = C & B is closed holds
C is closed
let D, B be Subset of X; :: thesis: for C being Subset of (X modified_with_respect_to D) st B = C & B is closed holds
C is closed
let C be Subset of (X modified_with_respect_to D); :: thesis: ( B = C & B is closed implies C is closed )
assume A1: B = C ; :: thesis: ( not B is closed or C is closed )
A2: the carrier of (X modified_with_respect_to D) = the carrier of X by TMAP_1:93;
assume B is closed ; :: thesis: C is closed
then C ` is open by A1, A2, Th1;
hence C is closed by TOPS_1:3; :: thesis: verum