let T be non empty TopSpace; :: thesis: for A being Subset of T st A is countable holds

for x being Point of T holds not x is_a_condensation_point_of A

let A be Subset of T; :: thesis: ( A is countable implies for x being Point of T holds not x is_a_condensation_point_of A )

assume A1: A is countable ; :: thesis: for x being Point of T holds not x is_a_condensation_point_of A

given x being Point of T such that A2: x is_a_condensation_point_of A ; :: thesis: contradiction

set N = the a_neighborhood of x;

not the a_neighborhood of x /\ A is countable by A2;

hence contradiction by A1, CARD_3:94; :: thesis: verum

for x being Point of T holds not x is_a_condensation_point_of A

let A be Subset of T; :: thesis: ( A is countable implies for x being Point of T holds not x is_a_condensation_point_of A )

assume A1: A is countable ; :: thesis: for x being Point of T holds not x is_a_condensation_point_of A

given x being Point of T such that A2: x is_a_condensation_point_of A ; :: thesis: contradiction

set N = the a_neighborhood of x;

not the a_neighborhood of x /\ A is countable by A2;

hence contradiction by A1, CARD_3:94; :: thesis: verum