let T be non empty TopSpace; :: thesis: for A being Subset of T holds A ^0 = Cl (A ^0 )
let A be Subset of T; :: thesis: A ^0 = Cl (A ^0 )
thus A ^0 c= Cl (A ^0 ) by PRE_TOPC:48; :: according to XBOOLE_0:def 10 :: thesis: Cl (A ^0 ) c= A ^0
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl (A ^0 ) or x in A ^0 )
assume A1: x in Cl (A ^0 ) ; :: thesis: x in A ^0
then reconsider p = x as Point of T ;
for N being a_neighborhood of p holds not N /\ A is countable

proof

let N be a_neighborhood of p; :: thesis: not N /\ A is countable
consider N1 being Subset of T such that
A2: ( N1 is open & N1 c= N & p in N1 ) by CONNSP_2:8;
A ^0 meets N1 by A1, A2, PRE_TOPC:54;
then consider y being set such that
A3: ( y in A ^0 & y in N1 ) by XBOOLE_0:3;
reconsider y' = y as Point of T by A3;
A4: y' is_a_condensation_point_of A by A3, Def10;
reconsider N1 = N1 as a_neighborhood of y' by A2, A3, CONNSP_2:8;
N1 /\ A c= N /\ A by A2, XBOOLE_1:26;
hence not N /\ A is countable by A4, Def9; :: thesis: verum

end;

then p is_a_condensation_point_of A by Def9;
hence x in A ^0 by Def10; :: thesis: verum