let G be _finite Path-like _Graph; :: thesis:
set H = the _trivial Subgraph of G;
consider p being non empty Graph-yielding _finite Path-like FinSequence such that
A1: ( p . 1 == the _trivial Subgraph of G & p . (len p) = G & len p = ((G .order()) - ( the _trivial Subgraph of G .order())) + 1 ) 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) & not v2 in the_Vertices_of (p . n) & ( not p . n is _trivial implies v1 in Endvertices (p . n) ) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) & ( not p . n is _trivial implies v2 in Endvertices (p . n) ) ) ) ) by Th22;
take p ; :: thesis:
thus ( p . 1 is _trivial & p . 1 is edgeless ) by A1, GLIB_008:52, GLIB_000:89; :: thesis:
thus p . (len p) = G by A1; :: thesis:
the _trivial Subgraph of G .order() = 1 by GLIB_000:26;
hence len p = G .order() by A1; :: thesis:
let n be Element of dom p; :: thesis:
assume A3: n <= (len p) - 1 ; :: thesis:
then consider v1, v2 being Vertex of G, e being object such that
A4: ( 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) & not v2 in the_Vertices_of (p . n) & ( not p . n is _trivial implies v1 in Endvertices (p . n) ) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) & ( not p . n is _trivial implies v2 in Endvertices (p . n) ) ) ) ) by A2;
take v1 ; :: thesis:
take v2 ; :: thesis:
take e ; :: thesis:
thus p . (n + 1) is addAdjVertex of p . n,v1,e,v2 by A4; :: thesis:
thus e in (the_Edges_of G) \ (the_Edges_of (p . n)) by A4; :: thesis:
( n >= 2 implies not p . n is _trivial )

proof

assume n >= 2 ; :: thesis:
then A6: n - 1 >= 2 - 1 by XREAL_1:9;
n - 1 <= n - 0 by XREAL_1:10;
then A7: n - 1 <= (len p) - 1 by A3, XXREAL_0:2;
(len p) - 1 <= (len p) - 0 by XREAL_1:10;
then A8: n - 1 <= len p by A7, XXREAL_0:2;
reconsider n1 = n - 1 as Element of NAT by A6, INT_1:3;
reconsider n1 = n1 as Element of dom p by A6, A8, FINSEQ_3:25;
consider w1, w2 being Vertex of G, e9 being object such that
A9: ( p . (n1 + 1) is addAdjVertex of p . n1,w1,e9,w2 & e9 in (the_Edges_of G) \ (the_Edges_of (p . n1)) & ( ( w1 in the_Vertices_of (p . n1) & not w2 in the_Vertices_of (p . n1) & ( not p . n1 is _trivial implies w1 in Endvertices (p . n1) ) ) or ( not w1 in the_Vertices_of (p . n1) & w2 in the_Vertices_of (p . n1) & ( not p . n1 is _trivial implies w2 in Endvertices (p . n1) ) ) ) ) by A2, A7;
not e9 in the_Edges_of (p . n1) by A9, XBOOLE_0:def 5;
hence not p . n is _trivial by A9, GLIB_006:143, GLIB_006:144; :: thesis:

end;

hence ( ( 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 A4; :: thesis: