let T be non empty TopSpace; :: thesis: for A being Subset of T st A is countable holds
A ^0 = {}
let A be Subset of T; :: thesis: ( A is countable implies A ^0 = {} )
assume A1: A is countable ; :: thesis: A ^0 = {}
assume A ^0 <> {} ; :: thesis: contradiction
then consider x being object such that
A2: x in A ^0 by XBOOLE_0:def 1;
reconsider x9 = x as Point of T by A2;
x9 is_a_condensation_point_of A by A2, Def10;
hence contradiction by A1, Th55; :: thesis: verum