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

proof

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;

hence x is_a_condensation_point_of B ; :: thesis: verum