:: deftheorem defines sequential FRECHET:def 7 :
for T being non empty TopStruct holds
( T is sequential iff for A being Subset of T holds
( A is closed iff for S being sequence of T st S is convergent & rng S c= A holds
Lim S c= A ) );