Let $X$ be a set $Y\subseteq X$ be non-empty. Then the filter generated by $Y$ is called a principal filter.
Show that $\mathcal{F}$ is a principal filter if and only if $\bigcap \mathcal{F}\in \mathcal{F}$.
My attempt: Let $\mathcal{F}$ be principal filter. Then there is a non-empty set $Y\subseteq X$ such that $\mathcal{F}=\{F: Y\subseteq F\}$. Thus $\bigcap \mathcal{F}=Y\in \mathcal{F}$.
Conversely, suppose $\bigcap \mathcal{F}\in \mathcal{F}$ and let $Y=\bigcap \mathcal{F}$. If $F\subseteq X$ such that $Y\subseteq F$, then by definition of a filter, we have $F\in \mathcal{F}$. On the other hand, if $F\in \mathcal{F}$, then $Y=\bigcap \mathcal{F}\subseteq F$, and we're done.
Is my proof correct?