Theorem reltrls

Description: The set ( TrailsG ) of all trails on G is a set of pairs by our definition of a trail, and so is a relation. (Contributed by AV, 29-Oct-2021)

	Ref	Expression
Assertion	reltrls	|- Rel ( Trails ` G )

Proof

Step	Hyp	Ref	Expression
1		df-trls	|- Trails = ( g e. _V |-> { <. f , p >. | ( f ( Walks ` g ) p /\ Fun `' f ) } )
2	1	relmptopab	|- Rel ( Trails ` G )