let G be _finite edgeless _Graph; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( 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; :: thesis: 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; :: thesis: verum