defpred S_{1}[ 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_{1}[x] )
and

A2: for x being Element of T holds

( x in A2 iff S_{1}[x] )
; :: thesis: A1 = A2

thus A1 = A2 from SUBSET_1:sch 2(A1, A2); :: thesis: verum

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

A2: for x being Element of T holds

( x in A2 iff S

thus A1 = A2 from SUBSET_1:sch 2(A1, A2); :: thesis: verum