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 = U. J
Assertion	sscls	|- ( ( J e. Top /\ S C_ X ) -> S C_ ( ( cls ` J ) ` S ) )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	|- X = U. J
2		ssintub	|- S C_ |^| { x e. ( Clsd ` J ) | S C_ x }
3	1	clsval	|- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) = |^| { x e. ( Clsd ` J ) | S C_ x } )
4	2 3	sseqtrrid	|- ( ( J e. Top /\ S C_ X ) -> S C_ ( ( cls ` J ) ` S ) )