let NT be NTopSpace; :: thesis: for A, B being Subset of NT st B = ([#] NT) \ A holds
([#] NT) \ (Cl A) = Int B
let A, B be Subset of NT; :: thesis: ( B = ([#] NT) \ A implies ([#] NT) \ (Cl A) = Int B )
assume A1: B = ([#] NT) \ A ; :: thesis: ([#] NT) \ (Cl A) = Int B

now :: thesis: ( ([#] NT) \ (Cl A) c= Int B & Int B c= ([#] NT) \ (Cl A) )

now :: thesis: for o being object st o in ([#] NT) \ (Cl A) holds
o in Int B

let o be object ; :: thesis: ( o in ([#] NT) \ (Cl A) implies o in Int B )
assume A2: o in ([#] NT) \ (Cl A) ; :: thesis: o in Int B
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 ;

now :: thesis: for x being object st x in V holds
x in ([#] NT) \ A

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

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: verum

end;

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

now :: thesis: for o being object st o in Int B holds
o in ([#] NT) \ (Cl A)

let o be object ; :: thesis: ( o in Int B implies o in ([#] NT) \ (Cl A) )
assume o in Int B ; :: thesis: o in ([#] NT) \ (Cl A)
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 }

proof

assume x in { x where x is Point of NT : x is_adherent_point_of A } ; :: thesis: contradiction
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: verum

end;

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

end;

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

end;

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