Theorem eupthiswlk

Description: An Eulerian path is a walk. (Contributed by AV, 6-Apr-2021)

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

Proof

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