Theorem crctiswlk

Description: A circuit is a walk. (Contributed by AV, 6-Apr-2021)

	Ref	Expression
Assertion	crctiswlk	$$⊢F\mathrm{Circuits}\left(G\right)P\to F\mathrm{Walks}\left(G\right)P$$

Proof

Step	Hyp	Ref	Expression
1		crctistrl	$$⊢F\mathrm{Circuits}\left(G\right)P\to F\mathrm{Trails}\left(G\right)P$$
2		trliswlk	$$⊢F\mathrm{Trails}\left(G\right)P\to F\mathrm{Walks}\left(G\right)P$$
3	1 2	syl	$$⊢F\mathrm{Circuits}\left(G\right)P\to F\mathrm{Walks}\left(G\right)P$$