let T be non empty TopSpace; :: thesis: for A being Subset of T
for p being Point of T st p is_a_condensation_point_of A holds
p is_an_accumulation_point_of A
let A be Subset of T; :: thesis: for p being Point of T st p is_a_condensation_point_of A holds
p is_an_accumulation_point_of A
let p be Point of T; :: thesis: ( p is_a_condensation_point_of A implies p is_an_accumulation_point_of A )
assume A1: p is_a_condensation_point_of A ; :: thesis: p is_an_accumulation_point_of A
for U being open Subset of T st p in U holds
ex q being Point of T st
( q <> p & q in A & q in U )

proof

let U be open Subset of T; :: thesis: ( p in U implies ex q being Point of T st
( q <> p & q in A & q in U ) )
assume p in U ; :: thesis: ex q being Point of T st
( q <> p & q in A & q in U )
then reconsider N = U as a_neighborhood of p by CONNSP_2:5;
reconsider NU = N /\ A as non empty non countable set by A1, Def9;
consider q being Element of NU such that
A2: p <> q by BORSUK_4:3;
q in NU ;
then reconsider q = q as Point of T ;
( q in A & q in U ) by XBOOLE_0:def 4;
hence ex q being Point of T st
( q <> p & q in A & q in U ) by A2; :: thesis: verum

end;

hence p is_an_accumulation_point_of A by TOPGEN_1:23; :: thesis: verum