Theorem llyssnlly

Description: A locally A space is n-locally A . (Contributed by Mario Carneiro, 2-Mar-2015)

	Ref	Expression
Assertion	llyssnlly	⊢ Locally 𝐴 ⊆ 𝑛-Locally 𝐴

Proof

Step	Hyp	Ref	Expression
1		llynlly	⊢ ( 𝑗 ∈ Locally 𝐴 → 𝑗 ∈ 𝑛-Locally 𝐴 )
2	1	ssriv	⊢ Locally 𝐴 ⊆ 𝑛-Locally 𝐴