Theorem erclwwlkrel

Description: .~ is a relation. (Contributed by Alexander van der Vekens, 25-Mar-2018) (Revised by AV, 29-Apr-2021)

	Ref	Expression
Hypothesis	erclwwlk.r	$$⊢\underset{\dot{}}{\sim }=\left\{⟨u,w⟩|\left(u\in \mathrm{ClWWalks}\left(G\right)\wedge w\in \mathrm{ClWWalks}\left(G\right)\wedge \exists n\in \left(0\dots \left|w\right|\right)u=w\mathrm{cyclShift}n\right)\right\}$$
Assertion	erclwwlkrel	$$⊢\mathrm{Rel}\underset{\dot{}}{\sim }$$

Proof

Step	Hyp	Ref	Expression
1		erclwwlk.r	$$⊢\underset{\dot{}}{\sim }=\left\{⟨u,w⟩|\left(u\in \mathrm{ClWWalks}\left(G\right)\wedge w\in \mathrm{ClWWalks}\left(G\right)\wedge \exists n\in \left(0\dots \left|w\right|\right)u=w\mathrm{cyclShift}n\right)\right\}$$
2	1	relopabi	$$⊢\mathrm{Rel}\underset{\dot{}}{\sim }$$