theorem :: GLIBPRE1:129

for G being loopless _Graph
for T being closed Trail of G st T is trivial holds
( T . 2 <> T . ((len T) - 1) & {(T . 2),(T . ((len T) - 1))} c= (T .first()) .edgesInOut() & 2 c= (T .first()) .degree() )