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