let A1, A2 be Subset of T; :: thesis: ( ( for x being Point of T holds
( x in A1 iff ex S being sequence of T st
( rng S c= A & x in Lim S ) ) ) & ( for x being Point of T holds
( x in A2 iff ex S being sequence of T st
( rng S c= A & x in Lim S ) ) ) implies A1 = A2 )
assume that
A1: for x being Point of T holds
( x in A1 iff ex S being sequence of T st
( rng S c= A & x in Lim S ) ) and
A2: for x being Point of T holds
( x in A2 iff ex S being sequence of T st
( rng S c= A & x in Lim S ) ) ; :: thesis: A1 = A2
for x being Point of T holds
( x in A1 iff x in A2 )

proof

let x be Point of T; :: thesis: ( x in A1 iff x in A2 )
( x in A1 iff ex S being sequence of T st
( rng S c= A & x in Lim S ) ) by A1;
hence ( x in A1 iff x in A2 ) by A2; :: thesis: verum

end;

hence A1 = A2 by SUBSET_1:3; :: thesis: verum