defpred S_{1}[ Element of T] means S is_convergent_to $1;

{ x where x is Element of T : S_{1}[x] } is Subset of T
from DOMAIN_1:sch 7();

then reconsider X = { x where x is Point of T : S_{1}[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

{ x where x is Element of T : S

then reconsider X = { x where x is Point of T : S

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