Theorem clwwlksswrd

Description: Closed walks (represented by words) are words. (Contributed by Alexander van der Vekens, 25-Mar-2018) (Revised by AV, 25-Apr-2021)

	Ref	Expression
Assertion	clwwlksswrd	$$⊢\mathrm{ClWWalks}\left(G\right)\subseteq \mathrm{Word}\mathrm{Vtx}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(G\right)$$
2		eqid	$$⊢\mathrm{Edg}\left(G\right)=\mathrm{Edg}\left(G\right)$$
3	1 2	clwwlk	$$⊢\mathrm{ClWWalks}\left(G\right)=\left\{w\in \mathrm{Word}\mathrm{Vtx}\left(G\right)|\left(w\ne \varnothing \wedge \forall i\in \left(0..^\left|w\right|-1\right)\left\{w\left(i\right),w\left(i+1\right)\right\}\in \mathrm{Edg}\left(G\right)\wedge \left\{\mathrm{lastS}\left(w\right),w\left(0\right)\right\}\in \mathrm{Edg}\left(G\right)\right)\right\}$$
4	3	ssrab3	$$⊢\mathrm{ClWWalks}\left(G\right)\subseteq \mathrm{Word}\mathrm{Vtx}\left(G\right)$$