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