defpred S₁[ Point of T] means $1 is_a_condensation_point_of A;
let A1, A2 be Subset of T; :: thesis: ( ( for x being Point of T holds
( x in A1 iff x is_a_condensation_point_of A ) ) & ( for x being Point of T holds
( x in A2 iff x is_a_condensation_point_of A ) ) implies A1 = A2 )
assume that
A1: for x being Element of T holds
( x in A1 iff S₁[x] ) and
A2: for x being Element of T holds
( x in A2 iff S₁[x] ) ; :: thesis: A1 = A2
thus A1 = A2 from SUBSET_1:sch 2(A1, A2); :: thesis: verum