Theorem cldss

Description: A closed set is a subset of the underlying set of a topology. (Contributed by NM, 5-Oct-2006) (Revised by Stefan O'Rear, 22-Feb-2015)

	Ref	Expression
Hypothesis	iscld.1	|- X = U. J
Assertion	cldss	|- ( S e. ( Clsd ` J ) -> S C_ X )

Proof

Step	Hyp	Ref	Expression
1		iscld.1	|- X = U. J
2		cldrcl	|- ( S e. ( Clsd ` J ) -> J e. Top )
3	1	iscld	|- ( J e. Top -> ( S e. ( Clsd ` J ) <-> ( S C_ X /\ ( X \ S ) e. J ) ) )
4	3	simprbda	|- ( ( J e. Top /\ S e. ( Clsd ` J ) ) -> S C_ X )
5	2 4	mpancom	|- ( S e. ( Clsd ` J ) -> S C_ X )