Metamath Proof Explorer


Theorem iscld4

Description: A subset is closed iff it contains its own closure. (Contributed by NM, 31-Jan-2008)

Ref Expression
Hypothesis clscld.1 X=J
Assertion iscld4 JTopSXSClsdJclsJSS

Proof

Step Hyp Ref Expression
1 clscld.1 X=J
2 1 iscld3 JTopSXSClsdJclsJS=S
3 eqss clsJS=SclsJSSSclsJS
4 1 sscls JTopSXSclsJS
5 4 biantrud JTopSXclsJSSclsJSSSclsJS
6 3 5 bitr4id JTopSXclsJS=SclsJSS
7 2 6 bitrd JTopSXSClsdJclsJSS