Metamath Proof Explorer


Theorem ntrss2

Description: A subset includes its interior. (Contributed by NM, 3-Oct-2007) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis clscld.1 X = J
Assertion ntrss2 J Top S X int J S S

Proof

Step Hyp Ref Expression
1 clscld.1 X = J
2 1 ntrval J Top S X int J S = J 𝒫 S
3 inss2 J 𝒫 S 𝒫 S
4 3 unissi J 𝒫 S 𝒫 S
5 unipw 𝒫 S = S
6 4 5 sseqtri J 𝒫 S S
7 2 6 eqsstrdi J Top S X int J S S