let NT be NTopSpace; :: thesis:
let A, B be Subset of NT; :: thesis:
assume A1: B = ([#] NT) \ A ; :: thesis:

let o be object ; :: thesis:
assume A2: o in ([#] NT) \ (Cl A) ; :: thesis:
then A3: ( o in [#] NT & not o in Cl A ) by XBOOLE_0:def 5;
reconsider x = o as Point of NT by A2, XBOOLE_0:def 5;
not x is_adherent_point_of A by A3;
then consider V being Element of U_FMT x such that
A4: not V meets A ;
reconsider V = V as Subset of NT ;

let x be object ; :: thesis:
assume A5: x in V ; :: thesis:
not x in A by A4, A5, XBOOLE_0:def 4;
hence x in ([#] NT) \ A by A5, XBOOLE_0:def 5; :: thesis:

end;

then A6: V c= ([#] NT) \ A ;
reconsider NA = ([#] NT) \ A as Subset of NT by XBOOLE_1:36;
NA in U_FMT x by A6, CARD_FIL:def 1;
then x is_interior_point_of NA by FINTOPO7:def 5;
hence o in Int B by A1; :: thesis:

end;

hence ([#] NT) \ (Cl A) c= Int B ; :: thesis:

let o be object ; :: thesis:
assume o in Int B ; :: thesis:
then consider x being Point of NT such that
A7: o = x and
A8: x is_interior_point_of B ;
A9: B in U_FMT x by A8, FINTOPO7:def 5;
not x in { x where x is Point of NT : x is_adherent_point_of A }

assume x in { x where x is Point of NT : x is_adherent_point_of A } ; :: thesis:
then consider y being Point of NT such that
A10: x = y and
A11: y is_adherent_point_of A ;
ex z being object st
( z in B & z in A ) by A9, A10, A11, XBOOLE_0:3;
hence contradiction by A1, XBOOLE_0:def 5; :: thesis:

end;

hence o in ([#] NT) \ (Cl A) by A7, XBOOLE_0:def 5; :: thesis:

end;

hence Int B c= ([#] NT) \ (Cl A) ; :: thesis:

end;

hence ([#] NT) \ (Cl A) = Int B ; :: thesis: