Theorem wlimss

Description: The class of limit points is a subclass of the base class. (Contributed by Scott Fenton, 16-Jun-2018)

	Ref	Expression
Assertion	wlimss	$$⊢WLim\left(R,A\right)\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		df-wlim	$$⊢WLim\left(R,A\right)=\left\{x\in A|\left(x\ne sup\left(A,A,R\right)\wedge x=sup\left(Pred\left(R,A,x\right),A,R\right)\right)\right\}$$
2	1	ssrab3	$$⊢WLim\left(R,A\right)\subseteq A$$