consider G2 being spanning Subgraph of G, p being non empty Graph-yielding _finite FinSequence such that
A2: H .size() = G2 .size() and
A3: ( p . 1 == H & p . (len p) = G2 & len p = ((G .order()) - (H .order())) + 1 ) and
A4: for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) by Th67;
consider q being non empty Graph-yielding _finite FinSequence such that
A5: ( q . 1 == G2 & q . (len q) = G & len q = ((G .size()) - (G2 .size())) + 1 ) and
A6: 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 Th64;
reconsider r = p ^' q as non empty Graph-yielding _finite FinSequence ;
take r ; :: thesis:
1 <= len p by FINSEQ_1:20;
hence r . 1 == H by A3, FINSEQ_6:140; :: thesis:
A7: 1 < len q

end;

hence r . (len r) = G by A5, FINSEQ_6:142; :: thesis:
(len r) + 1 = (len p) + (len q) by FINSEQ_6:139
.= ((((G .order()) + (G .size())) - ((H .order()) + (H .size()))) + 1) + 1 by A2, A3, A5 ;
hence len r = (((G .order()) + (G .size())) - ((H .order()) + (H .size()))) + 1 ; :: thesis:
let n be Element of dom r; :: thesis:
assume A8: 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;

then A10: ( n + 0 <= ((len p) - 1) + 1 & n + 1 <= ((len p) - 1) + 1 ) by XREAL_1:7;
A11: 1 <= n by FINSEQ_3:25;
then reconsider m = n as Element of dom p by A10, FINSEQ_3:25;
A12: r . n = p . m by A10, A11, FINSEQ_6:140;
1 + 0 <= n + 1 by XREAL_1:7;
then r . (n + 1) = p . (m + 1) by A10, FINSEQ_6:140;
hence ( 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) ) or ex v being Vertex of G st
( r . (n + 1) is addVertex of r . n,v & not v in the_Vertices_of (r . n) ) ) by A4, A9, A12; :: thesis:

end;

m + 1 <= len q by A7, 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
A16: ( 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 A6;
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 A14, A15, A5, A16, 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 A14, A16, A5, GLIB_000:def 34; :: thesis:

end;

hence ( 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) ) or ex v being Vertex of G st
( r . (n + 1) is addVertex of r . n,v & not v in the_Vertices_of (r . n) ) ) ; :: thesis:

end;

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

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 A19: 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 A18, FINSEQ_6:141;
then A20: r . (n + 1) = q . (((k1 + 1) + 1) + 1) ;
( 1 + 0 <= (k1 + 1) + 1 & (k1 + 1) + 1 <= len q ) by A18, XREAL_1:7;
then reconsider m = (k1 + 1) + 1 as Element of dom q by FINSEQ_3:25;

m + 1 <= len q by A18, 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
A21: ( 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 A6;
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 A19, A20, A21; :: thesis:

end;

then consider p being non empty Graph-yielding _finite FinSequence such that
A23: ( p . 1 == H & p . (len p) = G & len p = ((G .order()) - (H .order())) + 1 ) and
A24: for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) by Th60;
take p ; :: thesis:
thus ( p . 1 == H & p . (len p) = G ) by A23; :: thesis:
thus len p = (((G .order()) + (G .size())) - ((H .order()) + (H .size()))) + 1 by A22, A23; :: thesis:
let n be Element of dom p; :: thesis:
assume n <= (len p) - 1 ; :: thesis:
hence ( 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) ) or ex v being Vertex of G st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) by A24; :: thesis:

end;