theorem Th29: :: GLIB_016:29

for G being 1 -regular _Graph
for T being Trail of G st T is trivial holds
ex e being object st
( e Joins T .first() ,T .last() ,G & T = G .walkOf ((T .first()),e,(T .last())) )