Theorem sscls

Description: A subset of a topology's underlying set is included in its closure. (Contributed by NM, 22-Feb-2007)

	Ref	Expression
Hypothesis	clscld.1	$$⊢X=\bigcup J$$
Assertion	sscls	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq X\right)\to S\subseteq \mathrm{cls}\left(J\right)\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		clscld.1	$$⊢X=\bigcup J$$
2		ssintub	$$⊢S\subseteq \bigcap \left\{x\in \mathrm{Clsd}\left(J\right)|S\subseteq x\right\}$$
3	1	clsval	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq X\right)\to \mathrm{cls}\left(J\right)\left(S\right)=\bigcap \left\{x\in \mathrm{Clsd}\left(J\right)|S\subseteq x\right\}$$
4	2 3	sseqtrrid	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq X\right)\to S\subseteq \mathrm{cls}\left(J\right)\left(S\right)$$