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

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