Description: A closed walk of a fixed length as word is a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018) (Revised by AV, 24-Apr-2021) (Proof shortened by AV, 22-Mar-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | clwwlkclwwlkn | |- ( W e. ( N ClWWalksN G ) -> W e. ( ClWWalks ` G ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | isclwwlkn | |- ( W e. ( N ClWWalksN G ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) ) |
|
| 2 | 1 | simplbi | |- ( W e. ( N ClWWalksN G ) -> W e. ( ClWWalks ` G ) ) |