defpred S₁[ Nat] means for G1 being _finite non _trivial connected _Graph
for G2 being non spanning connected Subgraph of G1 st (G1 .order()) + $1 = (G1 .size()) + 1 holds
ex v being Vertex of G1 st
( not v is cut-vertex & not v in the_Vertices_of G2 );
A1: S₁[ 0 ]

proof

let G1 be _finite non _trivial connected _Graph; :: thesis: for G2 being non spanning connected Subgraph of G1 st (G1 .order()) + 0 = (G1 .size()) + 1 holds
ex v being Vertex of G1 st
( not v is cut-vertex & not v in the_Vertices_of G2 )
let G2 be non spanning connected Subgraph of G1; :: thesis: ( (G1 .order()) + 0 = (G1 .size()) + 1 implies ex v being Vertex of G1 st
( not v is cut-vertex & not v in the_Vertices_of G2 ) )
assume (G1 .order()) + 0 = (G1 .size()) + 1 ; :: thesis: ex v being Vertex of G1 st
( not v is cut-vertex & not v in the_Vertices_of G2 )
then G1 is Tree-like by GLIB_002:47;
then consider v being Vertex of G1 such that
A2: ( v is endvertex & not v in the_Vertices_of G2 ) by Th31;
thus ex v being Vertex of G1 st
( not v is cut-vertex & not v in the_Vertices_of G2 ) by A2; :: thesis: verum

end;

A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
let G1 be _finite non _trivial connected _Graph; :: thesis: for G2 being non spanning connected Subgraph of G1 st (G1 .order()) + (k + 1) = (G1 .size()) + 1 holds
ex v being Vertex of G1 st
( not v is cut-vertex & not v in the_Vertices_of G2 )
let G2 be non spanning connected Subgraph of G1; :: thesis: ( (G1 .order()) + (k + 1) = (G1 .size()) + 1 implies ex v being Vertex of G1 st
( not v is cut-vertex & not v in the_Vertices_of G2 ) )
assume A5: (G1 .order()) + (k + 1) = (G1 .size()) + 1 ; :: thesis: ex v being Vertex of G1 st
( not v is cut-vertex & not v in the_Vertices_of G2 )
not G1 is acyclic

proof

assume G1 is acyclic ; :: thesis: contradiction
then (k + 1) + ((G1 .size()) + 1) = 0 + ((G1 .size()) + 1) by A5, GLIB_002:46;
hence contradiction ; :: thesis: verum

end;

then consider C being Walk of G1 such that
A6: C is Cycle-like by GLIB_002:def 2;
ex e being set st
( e in C .edges() & ( C .edges() c= the_Edges_of G2 or not e in the_Edges_of G2 ) )

proof

per cases ( C .edges() c= the_Edges_of G2 or not C .edges() c= the_Edges_of G2 ) ;

suppose A7: C .edges() c= the_Edges_of G2 ; :: thesis: ex e being set st
( e in C .edges() & ( C .edges() c= the_Edges_of G2 or not e in the_Edges_of G2 ) )

set e = the Element of C .edges() ;
C .edges() <> {} by A6, GLIB_001:136;
then the Element of C .edges() in C .edges() ;
hence ex e being set st
( e in C .edges() & ( C .edges() c= the_Edges_of G2 or not e in the_Edges_of G2 ) ) by A7; :: thesis: verum

end;

suppose not C .edges() c= the_Edges_of G2 ; :: thesis: ex e being set st
( e in C .edges() & ( C .edges() c= the_Edges_of G2 or not e in the_Edges_of G2 ) )

then A8: (C .edges()) \ (the_Edges_of G2) <> {} by XBOOLE_1:37;
set e = the Element of (C .edges()) \ (the_Edges_of G2);
( the Element of (C .edges()) \ (the_Edges_of G2) in C .edges() & not the Element of (C .edges()) \ (the_Edges_of G2) in the_Edges_of G2 ) by A8, XBOOLE_0:def 5;
hence ex e being set st
( e in C .edges() & ( C .edges() c= the_Edges_of G2 or not e in the_Edges_of G2 ) ) ; :: thesis: verum

end;

end;

end;

then consider e being set such that
A9: e in C .edges() and
A10: ( C .edges() c= the_Edges_of G2 or not e in the_Edges_of G2 ) ;
set G3 = the removeEdge of G1,e;
reconsider G3 = the removeEdge of G1,e as non _trivial _Graph ;
reconsider G3 = G3 as _finite non _trivial connected _Graph by A6, A9, GLIB_002:5;
A11: the_Vertices_of G3 = the_Vertices_of G1 by GLIB_000:51;
A12: the_Edges_of G3 = (the_Edges_of G1) \ {e} by GLIB_000:51;
A13: (the_Edges_of G2) \ {e} c= the_Edges_of G3 by A12, XBOOLE_1:33;
set G4 = the removeEdge of G2,e;
reconsider G4 = the removeEdge of G2,e as Subgraph of G1 by GLIB_000:43;
A14: ( the_Vertices_of G4 = the_Vertices_of G2 & the_Edges_of G4 = (the_Edges_of G2) \ {e} ) by GLIB_000:51;
then reconsider G4 = G4 as Subgraph of G3 by A11, A13, GLIB_000:44;
G4 is connected

proof

per cases ( C .edges() c= the_Edges_of G2 or not e in the_Edges_of G2 ) by A10;

suppose A15: C .edges() c= the_Edges_of G2 ; :: thesis: G4 is connected

reconsider C2 = C as Walk of G2 by A6, A15, GLIB_001:169;
A16: C2 is Cycle-like by A6, GLIB_006:24;
e in C2 .edges() by A9, GLIB_001:110;
hence G4 is connected by A16, GLIB_002:5; :: thesis: verum

end;

suppose not e in the_Edges_of G2 ; :: thesis: G4 is connected

then the_Edges_of G4 = the_Edges_of G2 by A14, ZFMISC_1:57;
hence G4 is connected by A14, GLIB_000:86, GLIB_002:8; :: thesis: verum

end;

end;

end;

then reconsider G4 = G4 as connected Subgraph of G3 ;
not G4 is spanning

proof

assume G4 is spanning ; :: thesis: contradiction
then the_Vertices_of G2 = the_Vertices_of G1 by A11, A14, GLIB_000:def 33;
hence contradiction by GLIB_000:def 33; :: thesis: verum

end;

then reconsider G4 = G4 as non spanning connected Subgraph of G3 ;
((G1 .order()) + k) + 1 = ((G3 .size()) + 1) + 1 by A5, A9, GLIB_000:52;
then (G3 .order()) + k = (G3 .size()) + 1 by GLIB_000:52;
then consider v being Vertex of G3 such that
A17: ( not v is cut-vertex & not v in the_Vertices_of G4 ) by A4;
the_Vertices_of G3 c= the_Vertices_of G1 by GLIB_000:def 32;
then reconsider v0 = v as Vertex of G1 by TARSKI:def 3;
take v0 ; :: thesis: ( not v0 is cut-vertex & not v0 in the_Vertices_of G2 )

now :: thesis: for H1 being removeVertex of G1,v0 holds H1 .numComponents() c= G1 .numComponents()

let H1 be removeVertex of G1,v0; :: thesis: H1 .numComponents() c= G1 .numComponents()
set H2 = the removeVertex of G3,v;
A18: the removeVertex of G3,v .numComponents() c= G3 .numComponents() by A17, GLIB_002:35;
the removeVertex of G3,v is removeEdge of H1,e by GLIB_000:124;
then A19: H1 .numComponents() c= the removeVertex of G3,v .numComponents() by Lm8;
( G1 .numComponents() = 1 & G3 .numComponents() = 1 ) by GLIB_002:28;
hence H1 .numComponents() c= G1 .numComponents() by A18, A19, XBOOLE_1:1; :: thesis: verum

end;

hence not v0 is cut-vertex by GLIB_002:35; :: thesis: not v0 in the_Vertices_of G2
thus not v0 in the_Vertices_of G2 by A14, A17; :: thesis: verum

end;

A20: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A3);
let G1 be _finite non _trivial connected _Graph; :: thesis: for G2 being non spanning connected Subgraph of G1 ex v being Vertex of G1 st
( not v is cut-vertex & not v in the_Vertices_of G2 )
let G2 be non spanning connected Subgraph of G1; :: thesis: ex v being Vertex of G1 st
( not v is cut-vertex & not v in the_Vertices_of G2 )
ex k being Nat st (G1 .order()) + k = (G1 .size()) + 1 by GLIB_002:40, NAT_1:10;
hence ex v being Vertex of G1 st
( not v is cut-vertex & not v in the_Vertices_of G2 ) by A20; :: thesis: verum