let G be _Graph; :: thesis: for T being Trail of G
for n being odd Element of NAT st 1 < n & n < len T holds
ex v being Vertex of G st
( v = T . n & T . (n - 1) <> T . (n + 1) & {(T . (n - 1)),(T . (n + 1))} c= v .edgesInOut() & 2 c= v .degree() )
let T be Trail of G; :: thesis: for n being odd Element of NAT st 1 < n & n < len T holds
ex v being Vertex of G st
( v = T . n & T . (n - 1) <> T . (n + 1) & {(T . (n - 1)),(T . (n + 1))} c= v .edgesInOut() & 2 c= v .degree() )
let n9 be odd Element of NAT ; :: thesis: ( 1 < n9 & n9 < len T implies ex v being Vertex of G st
( v = T . n9 & T . (n9 - 1) <> T . (n9 + 1) & {(T . (n9 - 1)),(T . (n9 + 1))} c= v .edgesInOut() & 2 c= v .degree() ) )
assume A1: ( 1 < n9 & n9 < len T ) ; :: thesis: ex v being Vertex of G st
( v = T . n9 & T . (n9 - 1) <> T . (n9 + 1) & {(T . (n9 - 1)),(T . (n9 + 1))} c= v .edgesInOut() & 2 c= v .degree() )
reconsider n = n9 as odd Nat ;
consider m being odd Nat such that
A2: m + 2 = n by A1, Th5;
reconsider m = m as odd Element of NAT by ORDINAL1:def 12;
A4: T . (n + 1) Joins T . n,T . (n + 2),G by A1, GLIB_001:def 3;
A5: (m + 2) - 2 < n - 0 by A2, XREAL_1:15;
then m < len T by A1, XXREAL_0:2;
then A7: T . (m + 1) Joins T . n,T . m,G by A2, GLIB_001:def 3, GLIB_000:14;
then reconsider v = T . n as Vertex of G by GLIB_000:13;
take v ; :: thesis: ( v = T . n9 & T . (n9 - 1) <> T . (n9 + 1) & {(T . (n9 - 1)),(T . (n9 + 1))} c= v .edgesInOut() & 2 c= v .degree() )
thus v = T . n9 ; :: thesis: ( T . (n9 - 1) <> T . (n9 + 1) & {(T . (n9 - 1)),(T . (n9 + 1))} c= v .edgesInOut() & 2 c= v .degree() )
A8: n + 1 <= len T by A1, NAT_1:13;
A9: 0 + 1 <= m + 1 by XREAL_1:6;
m + 1 < n + 1 by A5, XREAL_1:8;
hence A10: T . (n9 - 1) <> T . (n9 + 1) by A2, A8, A9, GLIB_001:138; :: thesis: ( {(T . (n9 - 1)),(T . (n9 + 1))} c= v .edgesInOut() & 2 c= v .degree() )
( T . (m + 1) in v .edgesInOut() & T . (n + 1) in v .edgesInOut() ) by A4, A7, GLIB_000:62;
hence {(T . (n9 - 1)),(T . (n9 + 1))} c= v .edgesInOut() by A2, ZFMISC_1:32; :: thesis: 2 c= v .degree()
then card {(T . (n - 1)),(T . (n + 1))} c= card (v .edgesInOut()) by CARD_1:11;
then A11: 2 c= card (v .edgesInOut()) by A10, CARD_2:57;
card (v .edgesInOut()) c= (v .inDegree()) +` (v .outDegree()) by CARD_2:34;
hence 2 c= v .degree() by A11; :: thesis: verum