This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clsss3

Description: The closure of a subset of a topological space is included in the space. (Contributed by NM, 26-Feb-2007)

		Ref	Expression
	Hypothesis	clscld.1	$⊢ X = ⋃ J$
	Assertion	clsss3	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \subseteq X$

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2	1	clscld	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \in Clsd (J)$
3	1	cldss	$⊢ cls (J) (S) \in Clsd (J) \to cls (J) (S) \subseteq X$
4	2 3	syl	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \subseteq X$