let G be _finite connected _Graph; 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; 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 S1[ Nat] means for n being Element of dom p st $1 = n holds
p . n is connected ;
A3:
S1[1]
by A1, GLIB_002:8;
A4:
for k being non zero Nat st S1[k] holds
S1[k + 1]
A10:
for k being non zero Nat holds S1[k]
from NAT_1:sch 10(A3, A4);
for x being Element of dom p holds p . x is connected
then reconsider p = p as non empty Graph-yielding _finite connected FinSequence by GLIB_002:def 15;
take
p
; ( 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; verum