Description: The closed walks of a fixed length as words are closed walks (in an undirected graph) as words. (Contributed by Alexander van der Vekens, 15-Mar-2018) (Revised by AV, 12-Apr-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | clwwlksclwwlkn | |- ( N ClWWalksN G ) C_ ( ClWWalks ` G ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | clwwlkclwwlkn | |- ( w e. ( N ClWWalksN G ) -> w e. ( ClWWalks ` G ) ) |
|
| 2 | 1 | ssriv | |- ( N ClWWalksN G ) C_ ( ClWWalks ` G ) |