defpred S₁[ Point of T] means ex S being sequence of T st
( rng S c= A & $1 in Lim S );
reconsider X = { x where x is Point of T : S₁[x] } as Subset of T from DOMAIN_1:sch 7();
reconsider X = X as Subset of T ;
take X ; :: thesis: for x being Point of T 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 T; :: 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 x9 being Point of T st
( x = x9 & ex S being sequence of T st
( rng S c= A & x9 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