let T be non empty TopSpace; :: thesis: for A, B being Subset of T

for x being Point of T st x is_a_condensation_point_of A & A c= B holds

x is_a_condensation_point_of B

let A, B be Subset of T; :: thesis: for x being Point of T st x is_a_condensation_point_of A & A c= B holds

x is_a_condensation_point_of B

let x be Point of T; :: thesis: ( x is_a_condensation_point_of A & A c= B implies x is_a_condensation_point_of B )

assume that

A1: x is_a_condensation_point_of A and

A2: A c= B ; :: thesis: x is_a_condensation_point_of B

for N being a_neighborhood of x holds not N /\ B is countable

for x being Point of T st x is_a_condensation_point_of A & A c= B holds

x is_a_condensation_point_of B

let A, B be Subset of T; :: thesis: for x being Point of T st x is_a_condensation_point_of A & A c= B holds

x is_a_condensation_point_of B

let x be Point of T; :: thesis: ( x is_a_condensation_point_of A & A c= B implies x is_a_condensation_point_of B )

assume that

A1: x is_a_condensation_point_of A and

A2: A c= B ; :: thesis: x is_a_condensation_point_of B

for N being a_neighborhood of x holds not N /\ B is countable

proof

hence
x is_a_condensation_point_of B
; :: thesis: verum
let N be a_neighborhood of x; :: thesis: not N /\ B is countable

N /\ A c= N /\ B by A2, XBOOLE_1:26;

hence not N /\ B is countable by A1; :: thesis: verum

end;N /\ A c= N /\ B by A2, XBOOLE_1:26;

hence not N /\ B is countable by A1; :: thesis: verum