Metamath Proof Explorer


Theorem clwwlkclwwlkn

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 N ClWWalksN G W ClWWalks G

Proof

Step Hyp Ref Expression
1 isclwwlkn W N ClWWalksN G W ClWWalks G W = N
2 1 simplbi W N ClWWalksN G W ClWWalks G