defpred S₁[ Element of T] means S is_convergent_to $1;
{ x where x is Element of T : S₁[x] } is Subset of T from DOMAIN_1:sch 7();
then reconsider X = { x where x is Point of T : S₁[x] } as Subset of T ;
take X ; :: thesis: for x being Point of T holds
( x in X iff S is_convergent_to x )
let y be Point of T; :: thesis: ( y in X iff S is_convergent_to y )
( y in X iff ex x being Point of T st
( x = y & S is_convergent_to x ) ) ;
hence ( y in X iff S is_convergent_to y ) ; :: thesis: verum