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 )

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

hence
p is_an_accumulation_point_of A
by TOPGEN_1:21; :: thesis: verum
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:3;

reconsider NU = N /\ A as non empty non countable set by A1;

consider q being Element of NU such that

A2: p <> q by SUBSET_1:50;

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;( 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:3;

reconsider NU = N /\ A as non empty non countable set by A1;

consider q being Element of NU such that

A2: p <> q by SUBSET_1:50;

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