let A, B be Subset of T; :: thesis: ( ( for x being Point of T holds

( x in A iff S is_convergent_to x ) ) & ( for x being Point of T holds

( x in B iff S is_convergent_to x ) ) implies A = B )

assume that

A1: for x being Point of T holds

( x in A iff S is_convergent_to x ) and

A2: for x being Point of T holds

( x in B iff S is_convergent_to x ) ; :: thesis: A = B

for x being Point of T holds

( x in A iff x in B ) by A1, A2;

hence A = B by SUBSET_1:3; :: thesis: verum

( x in A iff S is_convergent_to x ) ) & ( for x being Point of T holds

( x in B iff S is_convergent_to x ) ) implies A = B )

assume that

A1: for x being Point of T holds

( x in A iff S is_convergent_to x ) and

A2: for x being Point of T holds

( x in B iff S is_convergent_to x ) ; :: thesis: A = B

for x being Point of T holds

( x in A iff x in B ) by A1, A2;

hence A = B by SUBSET_1:3; :: thesis: verum