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