defpred S₁[ Point of T] means $1 is_a_condensation_point_of A;
ex X being Subset of T st
for x being Element of T holds
( x in X iff S₁[x] ) from SUBSET_1:sch 3();
hence 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 ) ; :: thesis: verum