Metamath Proof Explorer


Theorem clstop

Description: The closure of a topology's underlying set is the entire set. (Contributed by NM, 5-Oct-2007) (Proof shortened by Jim Kingdon, 11-Mar-2023)

Ref Expression
Hypothesis clscld.1 X = J
Assertion clstop J Top cls J X = X

Proof

Step Hyp Ref Expression
1 clscld.1 X = J
2 1 topcld J Top X Clsd J
3 cldcls X Clsd J cls J X = X
4 2 3 syl J Top cls J X = X