Description: A subset includes its interior. (Contributed by NM, 3-Oct-2007) (Revised by Mario Carneiro, 11-Nov-2013)
Ref | Expression | ||
---|---|---|---|
Hypothesis | clscld.1 | ||
Assertion | ntrss2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clscld.1 | ||
2 | 1 | ntrval | |
3 | inss2 | ||
4 | 3 | unissi | |
5 | unipw | ||
6 | 4 5 | sseqtri | |
7 | 2 6 | eqsstrdi |