let G be _finite _Graph; :: thesis: ex p being non empty Graph-yielding _finite FinSequence st
( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = (G .order()) + (G .size()) & ( 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 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) ) ) ) )
set H = the _trivial edgeless Subgraph of G;
consider p being non empty Graph-yielding _finite FinSequence such that
A1: ( p . 1 == the _trivial edgeless Subgraph of G & p . (len p) = G ) and
A2: len p = (((G .order()) + (G .size())) - (( the _trivial edgeless Subgraph of G .order()) + ( the _trivial edgeless Subgraph of G .size()))) + 1 and
A3: 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 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 Th68;
take p ; :: thesis: ( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = (G .order()) + (G .size()) & ( 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 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) ) ) ) )
thus ( p . 1 is _trivial & p . 1 is edgeless ) by A1, Th52, GLIB_000:89; :: thesis: ( p . (len p) = G & len p = (G .order()) + (G .size()) & ( 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 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) ) ) ) )
thus p . (len p) = G by A1; :: thesis: ( len p = (G .order()) + (G .size()) & ( 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 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) ) ) ) )
thus len p = (((G .order()) + (G .size())) - (( the _trivial edgeless Subgraph of G .order()) + 0)) + 1 by A2, Th49
.= (((G .order()) + (G .size())) - 1) + 1 by GLIB_000:26
.= (G .order()) + (G .size()) ; :: thesis: 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 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) ) )
thus 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 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 A3; :: thesis: verum