Theorem spthiswlk

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

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

Proof

Step	Hyp	Ref	Expression
1		spthispth	$$⊢F\mathrm{SPaths}\left(G\right)P\to F\mathrm{Paths}\left(G\right)P$$
2		pthiswlk	$$⊢F\mathrm{Paths}\left(G\right)P\to F\mathrm{Walks}\left(G\right)P$$
3	1 2	syl	$$⊢F\mathrm{SPaths}\left(G\right)P\to F\mathrm{Walks}\left(G\right)P$$