defpred S₁[ Nat] means for G being _finite simple connected _Graph st G .order() = $1 holds
ex p being non empty Graph-yielding _finite simple connected 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 object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (p . n)) & V c= the_Vertices_of (p . n) & p . (n + 1) is addAdjVertexAll of p . n,v,V ) ) );
A1: S₁[1]

let G be _finite simple connected _Graph; :: thesis:
assume A2: G .order() = 1 ; :: thesis:
set p = <*G*>;
take <*G*> ; :: thesis:
G is _trivial by A2, GLIB_000:26;
hence ( <*G*> . 1 is _trivial & <*G*> . 1 is edgeless ) ; :: thesis:
thus <*G*> . (len <*G*>) = <*G*> . 1 by FINSEQ_1:40
.= G ; :: thesis:
thus len <*G*> = G .order() by A2, FINSEQ_1:40; :: thesis:
let n be Element of dom <*G*>; :: thesis:
( 1 <= n & n <= len <*G*> ) by FINSEQ_3:25;
then ( 1 <= n & n <= 1 ) by FINSEQ_1:40;
then A3: n = 1 by XXREAL_0:1;
assume n <= (len <*G*>) - 1 ; :: thesis:
then n <= 1 - 1 by FINSEQ_1:40;
hence ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (<*G*> . n)) & V c= the_Vertices_of (<*G*> . n) & <*G*> . (n + 1) is addAdjVertexAll of <*G*> . n,v,V ) by A3; :: thesis:

end;

A4: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

let k be non zero Nat; :: thesis:
assume A5: S₁[k] ; :: thesis:
let G be _finite simple connected _Graph; :: thesis:
assume A6: G .order() = k + 1 ; :: thesis:
A7: not G is _trivial

assume G is _trivial ; :: thesis:
then G .order() = 0 + 1 by GLIB_000:26;
hence contradiction by A6; :: thesis:

end;

then consider v9, v0 being Vertex of G such that
( v9 <> v0 & not v9 is cut-vertex ) and
A8: not v0 is cut-vertex by GLIB_002:37;
set G2 = the removeVertex of G,v0;
A9: ( the removeVertex of G,v0 .order()) + 1 = G .order() by A7, GLIB_000:48;
then A10: the removeVertex of G,v0 .order() = k by A6;
the removeVertex of G,v0 is connected by A8, GLIB_002:36;
then consider p being non empty Graph-yielding _finite simple connected FinSequence such that
A11: ( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = the removeVertex of G,v0 & len p = the removeVertex of G,v0 .order() ) and
A12: for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of the removeVertex of G,v0) \ (the_Vertices_of (p . n)) & V c= the_Vertices_of (p . n) & p . (n + 1) is addAdjVertexAll of p . n,v,V ) by A5, A10;
set q = p ^ <*G*>;
take p ^ <*G*> ; :: thesis:
1 in dom p by FINSEQ_5:6;
hence ( (p ^ <*G*>) . 1 is _trivial & (p ^ <*G*>) . 1 is edgeless ) by A11, FINSEQ_1:def 7; :: thesis:
A13: len (p ^ <*G*>) = (len p) + (len <*G*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:40 ;
hence A14: (p ^ <*G*>) . (len (p ^ <*G*>)) = G by FINSEQ_1:42; :: thesis:
thus len (p ^ <*G*>) = G .order() by A9, A11, A13; :: thesis:
let n be Element of dom (p ^ <*G*>); :: thesis:
assume n <= (len (p ^ <*G*>)) - 1 ; :: thesis:

per cases by Lm12;

suppose A15: n = (len (p ^ <*G*>)) - 1 ; :: thesis:

then A16: (p ^ <*G*>) . (n + 1) = G by A14;
A17: 1 <= n by FINSEQ_3:25;
A18: n = len p by A13, A15;
then n in dom p by A17, FINSEQ_3:25;
then A19: (p ^ <*G*>) . n = the removeVertex of G,v0 by A11, A18, FINSEQ_1:def 7;
reconsider V = v0 .allNeighbors() as non empty finite set by A7;
take v0 ; :: thesis:
take V ; :: thesis:
v0 in {v0} by TARSKI:def 1;
then not v0 in (the_Vertices_of G) \ {v0} by XBOOLE_0:def 5;
then not v0 in the_Vertices_of the removeVertex of G,v0 by A7, GLIB_000:47;
hence v0 in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n)) by A19, XBOOLE_0:def 5; :: thesis:
for x being object st x in V holds
x in the_Vertices_of the removeVertex of G,v0

let x be object ; :: thesis:
assume A20: x in V ; :: thesis:
then x <> v0 by GLIB_000:112;
then A21: not x in {v0} by TARSKI:def 1;
x in (the_Vertices_of G) \ {v0} by A20, A21, XBOOLE_0:def 5;
hence x in the_Vertices_of the removeVertex of G,v0 by A7, GLIB_000:47; :: thesis:

end;

hence V c= the_Vertices_of ((p ^ <*G*>) . n) by A19, TARSKI:def 3; :: thesis:
thus (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v0,V by A7, A16, A19, Th47; :: thesis:

end;

suppose A22: n <= (len p) - 1 ; :: thesis:

then A23: n + 0 <= ((len p) - 1) + 1 by XREAL_1:7;
1 <= n by FINSEQ_3:25;
then reconsider m = n as Element of dom p by A23, FINSEQ_3:25;
consider v being object , V being non empty finite set such that
A24: ( v in (the_Vertices_of the removeVertex of G,v0) \ (the_Vertices_of (p . m)) & V c= the_Vertices_of (p . m) & p . (m + 1) is addAdjVertexAll of p . m,v,V ) by A12, A22;
( 1 + 0 <= n + 1 & n + 1 <= ((len p) - 1) + 1 ) by A22, XREAL_1:6;
then n + 1 in dom p by FINSEQ_3:25;
then A25: (p ^ <*G*>) . (n + 1) = p . (m + 1) by FINSEQ_1:def 7;
A26: (p ^ <*G*>) . n = p . m by FINSEQ_1:def 7;
take v ; :: thesis:
take V ; :: thesis:
(the_Vertices_of the removeVertex of G,v0) \ (the_Vertices_of (p . m)) c= (the_Vertices_of G) \ (the_Vertices_of (p . m)) by XBOOLE_1:33;
hence v in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n)) by A24, A26; :: thesis:
thus ( V c= the_Vertices_of ((p ^ <*G*>) . n) & (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v,V ) by A24, A25, A26; :: thesis:

end;

end;

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A1, A4);
hence for G being _finite simple connected _Graph ex p being non empty Graph-yielding _finite simple connected 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 object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (p . n)) & V c= the_Vertices_of (p . n) & p . (n + 1) is addAdjVertexAll of p . n,v,V ) ) ) ; :: thesis: