Theorem erclwwlknrel

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

	Ref	Expression
Hypotheses	erclwwlkn.w	|- W = ( N ClWWalksN G )
	erclwwlkn.r	|- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
Assertion	erclwwlknrel	|- Rel .~

Proof

Step	Hyp	Ref	Expression
1		erclwwlkn.w	|- W = ( N ClWWalksN G )
2		erclwwlkn.r	|- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
3	2	relopabi	|- Rel .~