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 C_ N-Locally A

Proof

Step Hyp Ref Expression
1 llynlly 
 |-  ( j e. Locally A -> j e. N-Locally A )
2 1 ssriv 
 |-  Locally A C_ N-Locally A