defpred S₁[ set ] means $1 is_an_accumulation_point_of A;
consider D being Subset of T such that
A1: for x being set holds
( x in D iff ( x in the carrier of T & S₁[x] ) ) from SUBSET_1:sch 1();
take D ; :: thesis: for x being set st x in the carrier of T holds
( x in D iff x is_an_accumulation_point_of A )
thus for x being set st x in the carrier of T holds
( x in D iff x is_an_accumulation_point_of A ) by A1; :: thesis: verum