let G be 1 -regular _Graph; :: thesis: 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())) )
let T be Trail of G; :: thesis: ( T is trivial implies ex e being object st
( e Joins T .first() ,T .last() ,G & T = G .walkOf ((T .first()),e,(T .last())) ) )
assume T is trivial ; :: thesis: ex e being object st
( e Joins T .first() ,T .last() ,G & T = G .walkOf ((T .first()),e,(T .last())) )
then A1: 3 <= len T by GLIB_001:125;

now :: thesis: not len T <> 3

assume len T <> 3 ; :: thesis: contradiction
then A2: 3 < len T by A1, XXREAL_0:1;
then A3: T . (3 + 1) Joins T . 3,T . (3 + 2),G by GLIB_001:def 3, POLYFORM:6;
then reconsider v = T . 3 as Vertex of G by GLIB_000:13;
consider e being object such that
A4: ( v .edgesInOut() = {e} & not e Joins v,v,G ) by GLIB_000:def 51;
T . 4 in v .edgesInOut() by A3, GLIB_000:62;
then A5: T . 4 = e by A4, TARSKI:def 1;
1 < len T by A1, XXREAL_0:2;
then T . (1 + 1) Joins T . 1,T . (1 + 2),G by GLIB_001:def 3, POLYFORM:4;
then T . 2 in v .edgesInOut() by GLIB_000:14, GLIB_000:62;
then A6: T . 2 = T . 4 by A4, A5, TARSKI:def 1;
3 + 1 < (len T) + 1 by A2, XREAL_1:8;
then ( 1 <= 2 & 2 < 4 & 4 <= len T ) by NAT_1:13;
hence contradiction by A6, GLIB_001:138, POLYFORM:5, POLYFORM:7; :: thesis: verum

end;

hence ex e being object st
( e Joins T .first() ,T .last() ,G & T = G .walkOf ((T .first()),e,(T .last())) ) by GLIBPRE1:28; :: thesis: verum