let G be _finite edgeless _Graph; ex p being non empty Graph-yielding _finite edgeless FinSequence st
( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = G .order() & ( 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) ) ) )
set v0 = the Vertex of G;
set H = the inducedSubgraph of G,{ the Vertex of G};
consider p being non empty Graph-yielding _finite edgeless FinSequence such that
A1:
( p . 1 == the inducedSubgraph of G,{ the Vertex of G} & p . (len p) = G & len p = ((G .order()) - ( the inducedSubgraph of G,{ the Vertex of G} .order())) + 1 )
and
A2:
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 Th61;
take
p
; ( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = G .order() & ( 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) ) ) )
thus
( p . 1 is _trivial & p . 1 is edgeless )
by A1, Th52, GLIB_000:89; ( p . (len p) = G & len p = G .order() & ( 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) ) ) )
thus
p . (len p) = G
by A1; ( len p = G .order() & ( 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) ) ) )
the inducedSubgraph of G,{ the Vertex of G} .order() = 1
by GLIB_000:26;
hence
len p = G .order()
by A1; 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) )
thus
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 A2; verum