let G be _finite non _trivial Path-like _Graph; :: thesis:
consider p being non empty Graph-yielding _finite Path-like FinSequence such that
A1: ( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = G .order() ) and
A2: for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & ( ( v1 in the_Vertices_of (p . n) & ( n >= 2 implies v1 in Endvertices (p . n) ) & not v2 in the_Vertices_of (p . n) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) & ( n >= 2 implies v2 in Endvertices (p . n) ) ) ) ) by Th23;
A3: G .order() <> 1 by GLIB_000:26;
G .order() > 0 ;
then G .order() >= 0 + 1 by INT_1:7;
then G .order() > 1 by A3, XXREAL_0:1;
then A4: G .order() >= 1 + 1 by INT_1:7;
A5: len p >= 1 by FINSEQ_1:20;
then A6: len (p /^ 1) = (len p) - 1 by RFINSEQ:def 1;
then (len (p /^ 1)) + 1 = G .order() by A1;
then A7: len (p /^ 1) >= 1 by A4, XREAL_1:6;
then reconsider p1 = p /^ 1 as non empty Graph-yielding _finite Path-like FinSequence ;
take p1 ; :: thesis:
1 in dom p1 by A7, FINSEQ_3:25;
then A8: p1 . 1 = p . (1 + 1) by A5, RFINSEQ:def 1;
A9: (len p) - 1 >= (1 + 1) - 1 by A1, A4, XREAL_1:9;
reconsider k = 1 as Element of dom p by A5, FINSEQ_3:25;
consider v0, w0 being Vertex of G, e0 being object such that
A10: ( p . (k + 1) is addAdjVertex of p . k,v0,e0,w0 & e0 in (the_Edges_of G) \ (the_Edges_of (p . k)) & ( ( v0 in the_Vertices_of (p . k) & ( k >= 2 implies v0 in Endvertices (p . k) ) & not w0 in the_Vertices_of (p . k) ) or ( not v0 in the_Vertices_of (p . k) & w0 in the_Vertices_of (p . k) & ( k >= 2 implies w0 in Endvertices (p . k) ) ) ) ) by A2, A9;
A11: not e0 in the_Edges_of (p . k) by A10, XBOOLE_0:def 5;
reconsider G1 = p . (k + 1) as addAdjVertex of p . k,v0,e0,w0 by A10;
G1 .order() = ((p . k) .order()) + 1 by A10, A11, GLIB_006:152, GLIB_006:153
.= 1 + 1 by A1, GLIB_000:26 ;
hence p1 . 1 is 2 -vertex by A8, GLIB_013:def 3; :: thesis:
thus p1 . 1 is Path-like by A1, A8, A10, Th18, Th19; :: thesis:
len p1 in dom p1 by A7, FINSEQ_3:25;
hence p1 . (len p1) = p . (1 + (len p1)) by A5, RFINSEQ:def 1
.= G by A1, A6 ;
:: thesis:
thus (len p1) + 1 = G .order() by A1, A6; :: thesis:
let n be Element of dom p1; :: thesis:
assume n <= (len p1) - 1 ; :: thesis:
then A13: n + 1 <= (((len p) - 1) - 1) + 1 by A6, XREAL_1:6;
(len p) - 1 <= (len p) - 0 by XREAL_1:10;
then A14: n + 1 <= len p by A13, XXREAL_0:2;
A15: 1 <= n by FINSEQ_3:25;
A16: 1 + 0 <= n + 1 by XREAL_1:7;
then reconsider m = n + 1 as Element of dom p by A14, FINSEQ_3:25;
consider v1, v2 being Vertex of G, e being object such that
A17: ( p . (m + 1) is addAdjVertex of p . m,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . m)) & ( ( v1 in the_Vertices_of (p . m) & ( m >= 2 implies v1 in Endvertices (p . m) ) & not v2 in the_Vertices_of (p . m) ) or ( not v1 in the_Vertices_of (p . m) & v2 in the_Vertices_of (p . m) & ( m >= 2 implies v2 in Endvertices (p . m) ) ) ) ) by A2, A13;
take v1 ; :: thesis:
take v2 ; :: thesis:
take e ; :: thesis:
m in dom p1 by A6, A13, A16, FINSEQ_3:25;
then A18: p1 . m = p . (m + 1) by A5, RFINSEQ:def 1;
A19: p1 . n = p . (n + 1) by A5, RFINSEQ:def 1;
hence p1 . (n + 1) is addAdjVertex of p1 . n,v1,e,v2 by A17, A18; :: thesis:
thus e in (the_Edges_of G) \ (the_Edges_of (p1 . n)) by A17, A19; :: thesis:
m >= 1 + 1 by A15, XREAL_1:6;
hence ( ( v1 in Endvertices (p1 . n) & not v2 in the_Vertices_of (p1 . n) ) or ( not v1 in the_Vertices_of (p1 . n) & v2 in Endvertices (p1 . n) ) ) by A17, A19; :: thesis: