Metamath Proof Explorer

Theorem llyssnlly

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

Ref Expression
Assertion llyssnlly ⊢ Locally A ⊆ N-Locally A

Proof

Step Hyp Ref Expression
1 llynlly ⊢ j ∈ Locally A → j ∈ N-Locally A
2 1 ssriv ⊢ Locally A ⊆ N-Locally A