defpred S₁[ Point of ] means ex S being sequence of T st
( rng S c= A & $1 in Lim S );
reconsider X = { x where x is Point of : S₁[x] } as Subset of from DOMAIN_1:sch 7();
reconsider X = X as Subset of ;
take X ; :: thesis: for x being Point of holds
( x in X iff ex S being sequence of T st
( rng S c= A & x in Lim S ) )
let x be Point of ; :: thesis: ( x in X iff ex S being sequence of T st
( rng S c= A & x in Lim S ) )
thus ( x in X implies ex S being sequence of T st
( rng S c= A & x in Lim S ) ) :: thesis: ( ex S being sequence of T st
( rng S c= A & x in Lim S ) implies x in X )

proof

assume x in X ; :: thesis: ex S being sequence of T st
( rng S c= A & x in Lim S )
then ex x' being Point of st
( x = x' & ex S being sequence of T st
( rng S c= A & x' in Lim S ) ) ;
hence ex S being sequence of T st
( rng S c= A & x in Lim S ) ; :: thesis: verum

end;

assume ex S being sequence of T st
( rng S c= A & x in Lim S ) ; :: thesis: x in X
hence x in X ; :: thesis: verum