let X be non empty TopSpace; :: thesis: for Y0 being SubSpace of X
for A being Subset of X
for B being Subset of Y0 st B c= A holds
Cl B c= Cl A
let Y0 be SubSpace of X; :: thesis: for A being Subset of X
for B being Subset of Y0 st B c= A holds
Cl B c= Cl A
let A be Subset of X; :: thesis: for B being Subset of Y0 st B c= A holds
Cl B c= Cl A
let B be Subset of Y0; :: thesis: ( B c= A implies Cl B c= Cl A )
assume A1: B c= A ; :: thesis: Cl B c= Cl A
then reconsider D = B as Subset of X by XBOOLE_1:1;
Cl B = (Cl D) /\ ([#] Y0) by PRE_TOPC:17;
then A2: Cl B c= Cl D by XBOOLE_1:17;
Cl D c= Cl A by A1, PRE_TOPC:19;
hence Cl B c= Cl A by A2, XBOOLE_1:1; :: thesis: verum