defpred S₁[ object ] means $1 is_an_accumulation_point_of A;
let A1, A2 be Subset of T; :: thesis: ( ( for x being set st x in the carrier of T holds
( x in A1 iff x is_an_accumulation_point_of A ) ) & ( for x being set st x in the carrier of T holds
( x in A2 iff x is_an_accumulation_point_of A ) ) implies A1 = A2 )
assume that
A2: for x being set st x in the carrier of T holds
( x in A1 iff S₁[x] ) and
A3: for x being set st x in the carrier of T holds
( x in A2 iff S₁[x] ) ; :: thesis: A1 = A2
A4: A2 c= A1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A2 or x in A1 )
assume A5: x in A2 ; :: thesis: x in A1
then S₁[x] by A3;
hence x in A1 by A2, A5; :: thesis: verum

end;

A1 c= A2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A1 or x in A2 )
assume A6: x in A1 ; :: thesis: x in A2
then S₁[x] by A2;
hence x in A2 by A3, A6; :: thesis: verum

end;

hence A1 = A2 by A4; :: thesis: verum