let G be _finite connected _Graph; :: thesis: for H being spanning connected Subgraph of G ex p being non empty Graph-yielding _finite connected FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .size()) - (H .size())) + 1 & ( 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 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) ) ) )
let H be spanning connected Subgraph of G; :: thesis: ex p being non empty Graph-yielding _finite connected FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .size()) - (H .size())) + 1 & ( 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 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) ) ) )
consider p being non empty Graph-yielding _finite FinSequence such that
A1: ( p . 1 == H & p . (len p) = G & len p = ((G .size()) - (H .size())) + 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 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 Th64;
defpred S₁[ Nat] means for n being Element of dom p st $1 = n holds
p . n is connected ;
A3: S₁[1] by A1, GLIB_002:8;
A4: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
let m be Element of dom p; :: thesis: ( k + 1 = m implies p . m is connected )
assume A6: k + 1 = m ; :: thesis: p . m is connected
then A7: k + 1 <= len p by FINSEQ_3:25;
then A8: (k + 1) - 1 <= (len p) - 0 by XREAL_1:13;
1 <= k by NAT_1:14;
then reconsider n = k as Element of dom p by A8, FINSEQ_3:25;
(k + 1) - 1 <= (len p) - 1 by A7, XREAL_1:9;
then consider v1, v2 being Vertex of G, e being object such that
A9: ( 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 A2;
p . n is connected by A5;
hence p . m is connected by A6, A9; :: thesis: verum

end;

A10: for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A3, A4);
for x being Element of dom p holds p . x is connected

proof

let x be Element of dom p; :: thesis: p . x is connected
x is non zero Nat by FINSEQ_3:25;
hence p . x is connected by A10; :: thesis: verum

end;

then reconsider p = p as non empty Graph-yielding _finite connected FinSequence by GLIB_002:def 15;
take p ; :: thesis: ( p . 1 == H & p . (len p) = G & len p = ((G .size()) - (H .size())) + 1 & ( 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 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) ) ) )
thus ( p . 1 == H & p . (len p) = G & len p = ((G .size()) - (H .size())) + 1 & ( 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 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 A1, A2; :: thesis: verum