Metamath Proof Explorer


Theorem lpss

Description: The limit points of a subset are included in the base set. (Contributed by NM, 9-Nov-2007)

Ref Expression
Hypothesis lpfval.1 X=J
Assertion lpss JTopSXlimPtJSX

Proof

Step Hyp Ref Expression
1 lpfval.1 X=J
2 1 lpsscls JTopSXlimPtJSclsJS
3 1 clsss3 JTopSXclsJSX
4 2 3 sstrd JTopSXlimPtJSX