Theorem filelss

Description: An element of a filter is a subset of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015)

	Ref	Expression
Assertion	filelss	$$⊢\left(F\in \mathrm{Fil}\left(X\right)\wedge A\in F\right)\to A\subseteq X$$

Proof

Step	Hyp	Ref	Expression
1		filfbas	$$⊢F\in \mathrm{Fil}\left(X\right)\to F\in \mathrm{fBas}\left(X\right)$$
2		fbelss	$$⊢\left(F\in \mathrm{fBas}\left(X\right)\wedge A\in F\right)\to A\subseteq X$$
3	1 2	sylan	$$⊢\left(F\in \mathrm{Fil}\left(X\right)\wedge A\in F\right)\to A\subseteq X$$