Theorem filn0

Description: The empty set is not a filter. Remark below Definition 1 of BourbakiTop1 p. I.36. (Contributed by FL, 30-Oct-2007) (Revised by Stefan O'Rear, 28-Jul-2015)

	Ref	Expression
Assertion	filn0	$$⊢F\in \mathrm{Fil}\left(X\right)\to F\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		filtop	$$⊢F\in \mathrm{Fil}\left(X\right)\to X\in F$$
2	1	ne0d	$$⊢F\in \mathrm{Fil}\left(X\right)\to F\ne \varnothing$$