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 = U. J
Assertion	ntrss2	|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) C_ S )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	|- X = U. J
2	1	ntrval	|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) = U. ( J i^i ~P S ) )
3		inss2	|- ( J i^i ~P S ) C_ ~P S
4	3	unissi	|- U. ( J i^i ~P S ) C_ U. ~P S
5		unipw	|- U. ~P S = S
6	4 5	sseqtri	|- U. ( J i^i ~P S ) C_ S
7	2 6	eqsstrdi	|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) C_ S )