let T be non empty TopSpace; :: thesis: for A, B being Subset of T
for x being Point of T holds
( not x is_a_condensation_point_of A \/ B or x is_a_condensation_point_of A or x is_a_condensation_point_of B )
let A, B be Subset of T; :: thesis: for x being Point of T holds
( not x is_a_condensation_point_of A \/ B or x is_a_condensation_point_of A or x is_a_condensation_point_of B )
let x be Point of T; :: thesis: ( not x is_a_condensation_point_of A \/ B or x is_a_condensation_point_of A or x is_a_condensation_point_of B )
assume A1: x is_a_condensation_point_of A \/ B ; :: thesis: ( x is_a_condensation_point_of A or x is_a_condensation_point_of B )
assume that
A2: not x is_a_condensation_point_of A and
A3: not x is_a_condensation_point_of B ; :: thesis: contradiction
consider N1 being a_neighborhood of x such that
A4: N1 /\ A is countable by A2, Def9;
consider N2 being a_neighborhood of x such that
A5: N2 /\ B is countable by A3, Def9;
reconsider N3 = N1 /\ N2 as a_neighborhood of x by CONNSP_2:4;
B8: N3 /\ A c= N1 /\ A by XBOOLE_1:17, XBOOLE_1:26;
N3 /\ B c= N2 /\ B by XBOOLE_1:17, XBOOLE_1:26;
then (N3 /\ A) \/ (N3 /\ B) is countable by A4, A5, B8, CARD_3:128;
then N3 /\ (A \/ B) is countable by XBOOLE_1:23;
hence contradiction by A1, Def9; :: thesis: verum