let T be non empty TopSpace; :: thesis:
let A be Subset of T; :: thesis:
let p be Point of T; :: thesis:
assume A1: p is_a_condensation_point_of A ; :: thesis:
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 )

let U be open Subset of T; :: thesis:
assume p in U ; :: thesis:
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:

end;