let NT be NTopSpace; :: thesis: for A, B being Subset of NT st B = ([#] NT) \ A holds
([#] NT) \ (Int A) = Cl B
let A, B be Subset of NT; :: thesis: ( B = ([#] NT) \ A implies ([#] NT) \ (Int A) = Cl B )
assume A1: B = ([#] NT) \ A ; :: thesis: ([#] NT) \ (Int A) = Cl B
reconsider C = ([#] NT) \ B as Subset of NT by XBOOLE_1:36;
A2: ([#] NT) \ B = ([#] NT) /\ A by A1, XBOOLE_1:48
.= A by XBOOLE_1:28 ;
Cl B = ([#] NT) /\ (Cl B) by XBOOLE_1:28
.= ([#] NT) \ (([#] NT) \ (Cl B)) by XBOOLE_1:48
.= ([#] NT) \ (Int A) by A2, Lm14 ;
hence ([#] NT) \ (Int A) = Cl B ; :: thesis: verum