Theorem pthiswlk

Description: A path is a walk (in an undirected graph). (Contributed by AV, 6-Feb-2021)

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

Proof

Step	Hyp	Ref	Expression
1		pthistrl	$$⊢F\mathrm{Paths}\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{Paths}\left(G\right)P\to F\mathrm{Walks}\left(G\right)P$$