let G be loopless _Graph; :: thesis: 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() )
let T be closed Trail of G; :: thesis: ( T is trivial implies ( T . 2 <> T . ((len T) - 1) & {(T . 2),(T . ((len T) - 1))} c= (T .first()) .edgesInOut() & 2 c= (T .first()) .degree() ) )
assume T is trivial ; :: thesis: ( T . 2 <> T . ((len T) - 1) & {(T . 2),(T . ((len T) - 1))} c= (T .first()) .edgesInOut() & 2 c= (T .first()) .degree() )
then A1: 3 <= len T by GLIB_001:125;
then 1 < len T by XXREAL_0:2;
then T . (1 + 1) Joins T . 1,T . (1 + 2),G by POLYFORM:4, GLIB_001:def 3;
then A2: T . 2 Joins T .first() ,T . 3,G ;
3 - 2 <= (len T) - 2 by A1, XREAL_1:9;
then reconsider m = (len T) - 2 as Element of NAT by INT_1:3;
( m < (len T) - 0 & m is odd ) by XREAL_1:15, POLYFORM:5;
then T . (m + 1) Joins T . m,T . (m + 2),G by GLIB_001:def 3;
then T . ((len T) - 1) Joins T .last() ,T . m,G by GLIB_000:14;
then A4: T . ((len T) - 1) Joins T .first() ,T . m,G by GLIB_001:def 24;
thus A5: T . 2 <> T . ((len T) - 1) :: thesis: ( {(T . 2),(T . ((len T) - 1))} c= (T .first()) .edgesInOut() & 2 c= (T .first()) .degree() )

proof

assume A6: T . 2 = T . ((len T) - 1) ; :: thesis: contradiction
A7: 3 - 1 <= (len T) - 1 by A1, XREAL_1:9;
then reconsider k = (len T) - 1 as Element of NAT by INT_1:3;
k <= (len T) - 0 by XREAL_1:13;
then 2 >= k by A6, POLYFORM:5, GLIB_001:138;
then ((len T) - 1) + 1 = 2 + 1 by A7, XXREAL_0:1;
then consider e being object such that
A9: e Joins T .first() ,T .last() ,G and
T = G .walkOf ((T .first()),e,(T .last())) by Th28;
e Joins T .first() ,T .first() ,G by A9, GLIB_001:def 24;
hence contradiction by GLIB_000:18; :: thesis: verum

end;

set v = T .first() ;
( T . 2 in (T .first()) .edgesInOut() & T . ((len T) - 1) in (T .first()) .edgesInOut() ) by A2, A4, GLIB_000:62;
hence {(T . 2),(T . ((len T) - 1))} c= (T .first()) .edgesInOut() by ZFMISC_1:32; :: thesis: 2 c= (T .first()) .degree()
then card {(T . 2),(T . ((len T) - 1))} c= card ((T .first()) .edgesInOut()) by CARD_1:11;
then A10: 2 c= card ((T .first()) .edgesInOut()) by A5, CARD_2:57;
card ((T .first()) .edgesInOut()) c= ((T .first()) .inDegree()) +` ((T .first()) .outDegree()) by CARD_2:34;
hence 2 c= (T .first()) .degree() by A10, XBOOLE_1:1; :: thesis: verum