defpred S₁[ Point of T] means $1 is_a_condensation_point_of A;
consider X being Subset of T such that
A1: for x being Element of T holds
( x in X iff S₁[x] ) from SUBSET_1:sch 3();
thus ex b₁ being Subset of T st
for x being Point of T holds
( x in b₁ iff x is_a_condensation_point_of A ) by A1; :: thesis: verum