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:18; :: according to XBOOLE_0:def 10 :: thesis: Cl (A ^0) c= A ^0
let x be object ; :: 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 and
A3: N1 c= N and
A4: p in N1 by CONNSP_2:6;
A ^0 meets N1 by A1, A2, A4, PRE_TOPC:24;
then consider y being object such that
A5: y in A ^0 and
A6: y in N1 by XBOOLE_0:3;
reconsider y9 = y as Point of T by A5;
reconsider N1 = N1 as a_neighborhood of y9 by A2, A6, CONNSP_2:6;
A7: N1 /\ A c= N /\ A by A3, XBOOLE_1:26;
y9 is_a_condensation_point_of A by A5, Def10;
hence not N /\ A is countable by A7; :: thesis: verum

end;

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