Theorem flimnei

Description: A filter contains all of the neighborhoods of its limit points. (Contributed by Jeff Hankins, 4-Sep-2009) (Revised by Mario Carneiro, 9-Apr-2015)

	Ref	Expression
Assertion	flimnei	$$⊢\left(A\in \left(J\mathrm{fLim}F\right)\wedge N\in \mathrm{nei}\left(J\right)\left(\left\{A\right\}\right)\right)\to N\in F$$

Proof

Step	Hyp	Ref	Expression
1		flimneiss	$$⊢A\in \left(J\mathrm{fLim}F\right)\to \mathrm{nei}\left(J\right)\left(\left\{A\right\}\right)\subseteq F$$
2	1	sselda	$$⊢\left(A\in \left(J\mathrm{fLim}F\right)\wedge N\in \mathrm{nei}\left(J\right)\left(\left\{A\right\}\right)\right)\to N\in F$$