let NT be NTopSpace; :: thesis: for A being Subset of NT holds A c= Cl A
let A be Subset of NT; :: thesis: A c= Cl A
reconsider NCA = ([#] NT) \ (Cl A) as Subset of NT by XBOOLE_1:36;
reconsider NA = ([#] NT) \ A as Subset of NT by XBOOLE_1:36;
Int NA c= NA by Lm15;
then NCA c= NA by Lm14;
then ([#] NT) \ NA c= ([#] NT) \ NCA by XBOOLE_1:34;
then ([#] NT) /\ A c= ([#] NT) \ NCA by XBOOLE_1:48;
then A c= ([#] NT) \ NCA by XBOOLE_1:28;
then A c= ([#] NT) /\ (Cl A) by XBOOLE_1:48;
hence A c= Cl A by XBOOLE_1:28; :: thesis: verum