let NT be NTopSpace; :: thesis: for A, B being Subset of NT st A c= B holds
Cl A c= Cl B
let A, B be Subset of NT; :: thesis: ( A c= B implies Cl A c= Cl B )
assume A1: A c= B ; :: thesis: Cl A c= Cl B
reconsider NCA = ([#] NT) \ (Cl A) as Subset of NT by XBOOLE_1:36;
reconsider NCB = ([#] NT) \ (Cl B) as Subset of NT by XBOOLE_1:36;
reconsider NA = ([#] NT) \ A as Subset of NT by XBOOLE_1:36;
reconsider NB = ([#] NT) \ B as Subset of NT by XBOOLE_1:36;
( NB c= NA & NCA = Int NA & NCB = Int NB ) by Lm14, A1, XBOOLE_1:34;
then A2: NCB c= NCA by Lm17;

now :: thesis: ( Cl A = ([#] NT) \ NCA & Cl B = ([#] NT) \ NCB )

thus Cl A = ([#] NT) /\ (Cl A) by XBOOLE_1:28
.= ([#] NT) \ NCA by XBOOLE_1:48 ; :: thesis: Cl B = ([#] NT) \ NCB
thus Cl B = ([#] NT) /\ (Cl B) by XBOOLE_1:28
.= ([#] NT) \ NCB by XBOOLE_1:48 ; :: thesis: verum

end;

hence Cl A c= Cl B by A2, XBOOLE_1:34; :: thesis: verum