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

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

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

then
p is_a_condensation_point_of A
;
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;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

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