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;
consider N2 being a_neighborhood of x such that
A5: N2 /\ B is countable by A3;
reconsider N3 = N1 /\ N2 as a_neighborhood of x by CONNSP_2:2;
( N3 /\ A c= N1 /\ A & N3 /\ B c= N2 /\ B ) by XBOOLE_1:17, XBOOLE_1:26;
then (N3 /\ A) \/ (N3 /\ B) is countable by A4, A5, CARD_2:85;
then N3 /\ (A \/ B) is countable by XBOOLE_1:23;
hence contradiction by A1; :: thesis: verum