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

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