Theorem clwwlknlen

Description: The length of a word representing a closed walk of a fixed length is this fixed length. (Contributed by AV, 22-Mar-2022)

	Ref	Expression
Assertion	clwwlknlen	$$⊢W\in \left(N\mathrm{ClWWalksN}G\right)\to \left|W\right|=N$$

Proof

Step	Hyp	Ref	Expression
1		isclwwlkn	$$⊢W\in \left(N\mathrm{ClWWalksN}G\right)\leftrightarrow \left(W\in \mathrm{ClWWalks}\left(G\right)\wedge \left|W\right|=N\right)$$
2	1	simprbi	$$⊢W\in \left(N\mathrm{ClWWalksN}G\right)\to \left|W\right|=N$$