let X be non empty TopSpace; :: thesis: for Y0 being non empty closed SubSpace of X
for A being Subset of X
for B being Subset of Y0 st A = B holds
Cl A = Cl B
let Y0 be non empty closed SubSpace of X; :: thesis: for A being Subset of X
for B being Subset of Y0 st A = B holds
Cl A = Cl B
reconsider C = the carrier of Y0 as Subset of X by TSEP_1:1;
let A be Subset of X; :: thesis: for B being Subset of Y0 st A = B holds
Cl A = Cl B
let B be Subset of Y0; :: thesis: ( A = B implies Cl A = Cl B )
A1: C is closed by TSEP_1:11;
assume A = B ; :: thesis: Cl A = Cl B
hence Cl A = Cl B by A1, Th54; :: thesis: verum