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