let G be _finite connected _Graph; :: thesis:

suppose A1: not G is acyclic ; :: thesis:

set H = the spanning Tree-like Subgraph of G;
consider p being non empty Graph-yielding _finite Tree-like FinSequence such that
A2: ( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = the spanning Tree-like Subgraph of G & len p = the spanning Tree-like Subgraph of G .order() ) and
A3: for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of the spanning Tree-like Subgraph of G ex e being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & e in (the_Edges_of the spanning Tree-like Subgraph of G) \ (the_Edges_of (p . n)) & ( ( v1 in the_Vertices_of (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) ) ) ) by Th72;
consider q being non empty Graph-yielding _finite connected FinSequence such that
A4: ( q . 1 == the spanning Tree-like Subgraph of G & q . (len q) = G & len q = ((G .size()) - ( the spanning Tree-like Subgraph of G .size())) + 1 ) and
A5: for n being Element of dom q st n <= (len q) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( q . (n + 1) is addEdge of q . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (q . n)) & v1 in the_Vertices_of (q . n) & v2 in the_Vertices_of (q . n) ) by Th66;
reconsider r = p ^' q as non empty Graph-yielding _finite connected FinSequence ;
take r ; :: thesis:
1 <= len p by FINSEQ_1:20;
hence ( r . 1 is _trivial & r . 1 is edgeless ) by A2, FINSEQ_6:140; :: thesis:
A6: 1 < len q

proof

assume not 1 < len q ; :: thesis:
then ( len q <= 1 & 1 <= len q ) by FINSEQ_1:20;
then G == the spanning Tree-like Subgraph of G by A4, XXREAL_0:1;
hence contradiction by A1, GLIB_002:44; :: thesis:

end;

hence r . (len r) = G by A4, FINSEQ_6:142; :: thesis:
(len r) + 1 = (len p) + (len q) by FINSEQ_6:139
.= ((( the spanning Tree-like Subgraph of G .order()) + (G .size())) - ( the spanning Tree-like Subgraph of G .size())) + 1 by A2, A4
.= (((( the spanning Tree-like Subgraph of G .size()) + 1) + (G .size())) - ( the spanning Tree-like Subgraph of G .size())) + 1 by GLIB_002:46
.= ((G .size()) + 1) + 1 ;
hence len r = (G .size()) + 1 ; :: thesis:
let n be Element of dom r; :: thesis:
assume A7: n <= (len r) - 1 ; :: thesis:
( n < len p or n = len p or n > len p ) by XXREAL_0:1;
then ( n + 1 <= len p or n = len p or n > len p ) by INT_1:7;
then ( (n + 1) - 1 <= (len p) - 1 or n = len p or n > len p ) by XREAL_1:9;

per cases ;

suppose A8: n <= (len p) - 1 ; :: thesis:

then A9: ( n + 0 <= ((len p) - 1) + 1 & n + 1 <= ((len p) - 1) + 1 ) by XREAL_1:7;
A10: 1 <= n by FINSEQ_3:25;
then reconsider m = n as Element of dom p by A9, FINSEQ_3:25;
A11: r . n = p . m by A9, A10, FINSEQ_6:140;
1 + 0 <= n + 1 by XREAL_1:7;
then A12: r . (n + 1) = p . (m + 1) by A9, FINSEQ_6:140;

now :: thesis:

consider v1, v2 being Vertex of the spanning Tree-like Subgraph of G, e being object such that
A13: ( p . (m + 1) is addAdjVertex of p . m,v1,e,v2 & e in (the_Edges_of the spanning Tree-like Subgraph of G) \ (the_Edges_of (p . m)) & ( ( v1 in the_Vertices_of (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) ) ) ) by A3, A8;
the_Vertices_of the spanning Tree-like Subgraph of G c= the_Vertices_of G ;
then reconsider v1 = v1, v2 = v2 as Vertex of G by TARSKI:def 3;
take v1 = v1; :: thesis:
take v2 = v2; :: thesis:
take e = e; :: thesis:
(the_Edges_of the spanning Tree-like Subgraph of G) \ (the_Edges_of (p . m)) c= (the_Edges_of G) \ (the_Edges_of (p . m)) by XBOOLE_1:33;
hence ( r . (n + 1) is addAdjVertex of r . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (r . n)) & ( ( v1 in the_Vertices_of (r . n) & not v2 in the_Vertices_of (r . n) ) or ( not v1 in the_Vertices_of (r . n) & v2 in the_Vertices_of (r . n) ) ) ) by A11, A12, A13; :: thesis:

end;

hence ( ex v1, v2 being Vertex of G ex e being object st
( r . (n + 1) is addAdjVertex of r . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (r . n)) & ( ( v1 in the_Vertices_of (r . n) & not v2 in the_Vertices_of (r . n) ) or ( not v1 in the_Vertices_of (r . n) & v2 in the_Vertices_of (r . n) ) ) ) or ex v1, v2 being Vertex of G ex e being object st
( r . (n + 1) is addEdge of r . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (r . n)) & v1 in the_Vertices_of (r . n) & v2 in the_Vertices_of (r . n) ) ) ; :: thesis:

end;

suppose A14: n = len p ; :: thesis:

then ( 1 <= n & n <= len p ) by FINSEQ_1:20;
then A15: r . n = the spanning Tree-like Subgraph of G by A2, A14, FINSEQ_6:140;
reconsider m = 1 as Element of dom q by A6, FINSEQ_3:25;
A16: r . (n + 1) = q . (m + 1) by A14, A6, FINSEQ_6:141;

now :: thesis:

m + 1 <= len q by A6, INT_1:7;
then (m + 1) - 1 <= (len q) - 1 by XREAL_1:9;
then consider v1, v2 being Vertex of G, e being object such that
A17: ( q . (m + 1) is addEdge of q . m,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (q . m)) & v1 in the_Vertices_of (q . m) & v2 in the_Vertices_of (q . m) ) by A5;
take v1 = v1; :: thesis:
take v2 = v2; :: thesis:
take e = e; :: thesis:
thus r . (n + 1) is addEdge of r . n,v1,e,v2 by A4, A15, A16, A17, Th36; :: thesis:
thus ( e in (the_Edges_of G) \ (the_Edges_of (r . n)) & v1 in the_Vertices_of (r . n) & v2 in the_Vertices_of (r . n) ) by A4, A15, A17, GLIB_000:def 34; :: thesis:

end;

suppose A18: n > len p ; :: thesis:

then reconsider n1 = n - 1 as Nat by NAT_1:20;
n1 + 1 = n ;
then len p <= n1 by A18, NAT_1:13;
then reconsider k1 = n1 - (len p) as Nat by NAT_1:21;
set k = k1 + 1;
A19: (k1 + 1) + 1 < len q

proof

assume len q <= (k1 + 1) + 1 ; :: thesis:
then (len q) + (len p) <= ((k1 + 1) + 1) + (len p) by XREAL_1:6;
then (len r) + 1 <= n + 1 by FINSEQ_6:139;
then (len r) - 1 <= n - 1 by XREAL_1:6, XREAL_1:9;
then n <= n - 1 by A7, XXREAL_0:2;
then n - n <= (n - 1) - n by XREAL_1:9;
then 0 <= - 1 ;
hence contradiction ; :: thesis:

end;

then ((k1 + 1) + 1) - 1 < (len q) - 0 by XREAL_1:14;
then r . ((len p) + (k1 + 1)) = q . ((k1 + 1) + 1) by NAT_1:14, FINSEQ_6:141;
then A20: r . n = q . ((k1 + 1) + 1) ;
1 + 0 <= (k1 + 1) + 1 by XREAL_1:7;
then r . ((len p) + ((k1 + 1) + 1)) = q . (((k1 + 1) + 1) + 1) by A19, FINSEQ_6:141;
then A21: r . (n + 1) = q . (((k1 + 1) + 1) + 1) ;
( 1 + 0 <= (k1 + 1) + 1 & (k1 + 1) + 1 <= len q ) by A19, XREAL_1:7;
then reconsider m = (k1 + 1) + 1 as Element of dom q by FINSEQ_3:25;

now :: thesis:

m + 1 <= len q by A19, INT_1:7;
then (m + 1) - 1 <= (len q) - 1 by XREAL_1:9;
then consider v1, v2 being Vertex of G, e being object such that
A22: ( q . (m + 1) is addEdge of q . m,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (q . m)) & v1 in the_Vertices_of (q . m) & v2 in the_Vertices_of (q . m) ) by A5;
take v1 = v1; :: thesis:
take v2 = v2; :: thesis:
take e = e; :: thesis:
thus ( r . (n + 1) is addEdge of r . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (r . n)) & v1 in the_Vertices_of (r . n) & v2 in the_Vertices_of (r . n) ) by A20, A21, A22; :: thesis:

end;

suppose A23: G is acyclic ; :: thesis:

then consider p being non empty Graph-yielding _finite Tree-like FinSequence such that
A24: ( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = G .order() ) and
A25: 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) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) ) by Th72;
take p ; :: thesis:
thus ( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = (G .size()) + 1 & ( for n being Element of dom p holds
( not n <= (len p) - 1 or 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) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) ) or ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) ) ) by A24, A25, A23, GLIB_002:46; :: thesis:

end;