Metamath Proof Explorer


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=J
Assertion sscls JTopSXSclsJS

Proof

Step Hyp Ref Expression
1 clscld.1 X=J
2 ssintub SxClsdJ|Sx
3 1 clsval JTopSXclsJS=xClsdJ|Sx
4 2 3 sseqtrrid JTopSXSclsJS