defpred S₁[ Nat] means for G being _finite Tree-like _Graph
for H being connected Subgraph of G st $1 = (G .order()) - (H .order()) holds
ex p being non empty Graph-yielding _finite Tree-like FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .order()) - (H .order())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & ( ( v1 in the_Vertices_of (p . n) & not v2 in the_Vertices_of (p . n) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) ) ) );
A1: S₁[ 0 ]

proof

let G be _finite Tree-like _Graph; :: thesis:
let H be connected Subgraph of G; :: thesis:
assume A2: 0 = (G .order()) - (H .order()) ; :: thesis:
then H is spanning by GLIB_000:117;
then A3: G == H by Th21;
reconsider p = <*G*> as non empty Graph-yielding _finite Tree-like FinSequence ;
take p ; :: thesis:
thus p . 1 == H by A3; :: thesis:
thus p . (len p) = p . 1 by FINSEQ_1:40
.= G ; :: thesis:
thus len p = ((G .order()) - (H .order())) + 1 by A2, FINSEQ_1:40; :: thesis:
let n be Element of dom p; :: thesis:
( 1 <= n & n <= len p ) by FINSEQ_3:25;
then ( 1 <= n & n <= 1 ) by FINSEQ_1:40;
then A4: n = 1 by XXREAL_0:1;
assume n <= (len p) - 1 ; :: thesis:
then n <= 1 - 1 by FINSEQ_1:40;
hence ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & ( ( v1 in the_Vertices_of (p . n) & not v2 in the_Vertices_of (p . n) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) ) by A4; :: thesis:

end;

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

proof

let k be Nat; :: thesis:
assume A6: S₁[k] ; :: thesis:
let G be _finite Tree-like _Graph; :: thesis:
let H be connected Subgraph of G; :: thesis:
assume A7: k + 1 = (G .order()) - (H .order()) ; :: thesis:
then A8: G .order() = ((H .order()) + k) + 1 ;
G .order() <> H .order()

proof

assume G .order() = H .order() ; :: thesis:
then 0 + (H .order()) = (k + 1) + (H .order()) by A8;
hence contradiction ; :: thesis:

end;

then A9: not H is spanning by GLIB_000:117;
G .order() <> 1 by A8, NAT_1:7;
then A10: not G is _trivial by GLIB_000:26;
then consider v being Vertex of G such that
A11: ( v is endvertex & not v in the_Vertices_of H ) by A9, Th31;
consider e0 being object such that
A12: ( v .edgesInOut() = {e0} & not e0 Joins v,v,G ) by A11, GLIB_000:def 51;
set G2 = the removeVertex of G,v;
A13: ( the removeVertex of G,v .order()) + 1 = G .order() by A10, GLIB_000:48;
then A14: k = ( the removeVertex of G,v .order()) - (H .order()) by A7;
A15: the_Edges_of the removeVertex of G,v = G .edgesBetween ((the_Vertices_of G) \ {v}) by A10, GLIB_000:47
.= (G .edgesBetween (the_Vertices_of G)) \ (v .edgesInOut()) by GLIB_000:107
.= (the_Edges_of G) \ {e0} by A12, GLIB_000:34 ;
A16: H is Subgraph of the removeVertex of G,v

proof

the_Vertices_of H misses {v} by A11, ZFMISC_1:50;
then the_Vertices_of H c= (the_Vertices_of G) \ {v} by XBOOLE_1:86;
then A17: the_Vertices_of H c= the_Vertices_of the removeVertex of G,v by A10, GLIB_000:47;
not e0 in the_Edges_of H

proof

assume A18: e0 in the_Edges_of H ; :: thesis:
e0 in v .edgesInOut() by A12, TARSKI:def 1;

per cases ) . e0 = v or (the_Target_of G) . e0 = v ) by GLIB_000:61;

suppose (the_Source_of G) . e0 = v ; :: thesis:

then (the_Source_of H) . e0 = v by A18, GLIB_000:def 32;
hence contradiction by A11, A18, FUNCT_2:5; :: thesis:

end;

suppose (the_Target_of G) . e0 = v ; :: thesis:

then (the_Target_of H) . e0 = v by A18, GLIB_000:def 32;
hence contradiction by A11, A18, FUNCT_2:5; :: thesis:

end;

then the_Edges_of H misses {e0} by ZFMISC_1:50;
hence H is Subgraph of the removeVertex of G,v by A15, A17, GLIB_000:44, XBOOLE_1:86; :: thesis:

end;

consider p being non empty Graph-yielding _finite Tree-like FinSequence such that
A19: ( p . 1 == H & p . (len p) = the removeVertex of G,v & len p = (( the removeVertex of G,v .order()) - (H .order())) + 1 ) and
A20: for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of the removeVertex of G,v ex e being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & e in (the_Edges_of the removeVertex of G,v) \ (the_Edges_of (p . n)) & ( ( v1 in the_Vertices_of (p . n) & not v2 in the_Vertices_of (p . n) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) ) by A6, A14, A16, A10, A11;
reconsider q = p ^ <*G*> as non empty Graph-yielding _finite Tree-like FinSequence ;
take q ; :: thesis:
1 in dom p by FINSEQ_5:6;
hence q . 1 == H by A19, FINSEQ_1:def 7; :: thesis:
A21: len q = (len p) + (len <*G*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:40 ;
hence A22: q . (len q) = G by FINSEQ_1:42; :: thesis:
thus len q = ((G .order()) - (H .order())) + 1 by A13, A19, A21; :: thesis:
let n be Element of dom q; :: thesis:
assume n <= (len q) - 1 ; :: thesis:

per cases by Lm12;

suppose A23: n = (len q) - 1 ; :: thesis:

then A24: q . (n + 1) = G by A22;
1 <= n by FINSEQ_3:25;
then n in dom p by A21, A23, FINSEQ_3:25;
then A27: q . n = the removeVertex of G,v by A19, A21, A23, FINSEQ_1:def 7;
A28: e0 in v .edgesInOut() by A12, TARSKI:def 1;
then A29: e0 in the_Edges_of G ;
e0 in {e0} by TARSKI:def 1;
then A30: not e0 in the_Edges_of (q . n) by A15, A27, XBOOLE_0:def 5;
v in {v} by TARSKI:def 1;
then not v in (the_Vertices_of G) \ {v} by XBOOLE_0:def 5;
then A31: not v in the_Vertices_of (q . n) by A10, A27, GLIB_000:47;
v .adj e0 <> v by A12, A28, GLIB_000:67;
then not v .adj e0 in {v} by TARSKI:def 1;
then v .adj e0 in (the_Vertices_of G) \ {v} by XBOOLE_0:def 5;
then A32: v .adj e0 in the_Vertices_of (q . n) by A10, A27, GLIB_000:47;

per cases by A10, A12, Th38;

suppose A33: G is addAdjVertex of the removeVertex of G,v,v .adj e0,e0,v ; :: thesis:

take v .adj e0 ; :: thesis:
take v ; :: thesis:
take e0 ; :: thesis:
thus q . (n + 1) is addAdjVertex of q . n,v .adj e0,e0,v by A24, A27, A33; :: thesis:
thus ( e0 in (the_Edges_of G) \ (the_Edges_of (q . n)) & ( ( v .adj e0 in the_Vertices_of (q . n) & not v in the_Vertices_of (q . n) ) or ( not v .adj e0 in the_Vertices_of (q . n) & v in the_Vertices_of (q . n) ) ) ) by A29, A30, A31, A32, XBOOLE_0:def 5; :: thesis:

end;

suppose A34: G is addAdjVertex of the removeVertex of G,v,v,e0,v .adj e0 ; :: thesis:

take v ; :: thesis:
take v .adj e0 ; :: thesis:
take e0 ; :: thesis:
thus q . (n + 1) is addAdjVertex of q . n,v,e0,v .adj e0 by A24, A27, A34; :: thesis:
thus ( e0 in (the_Edges_of G) \ (the_Edges_of (q . n)) & ( ( v in the_Vertices_of (q . n) & not v .adj e0 in the_Vertices_of (q . n) ) or ( not v in the_Vertices_of (q . n) & v .adj e0 in the_Vertices_of (q . n) ) ) ) by A29, A30, A31, A32, XBOOLE_0:def 5; :: thesis:

end;

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

then A36: 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 A36, FINSEQ_3:25;
consider v1, v2 being Vertex of the removeVertex of G,v, e being object such that
A37: ( p . (m + 1) is addAdjVertex of p . m,v1,e,v2 & e in (the_Edges_of the removeVertex of G,v) \ (the_Edges_of (p . m)) & ( ( v1 in the_Vertices_of (p . m) & not v2 in the_Vertices_of (p . m) ) or ( not v1 in the_Vertices_of (p . m) & v2 in the_Vertices_of (p . m) ) ) ) by A20, A35;
( 1 + 0 <= n + 1 & n + 1 <= ((len p) - 1) + 1 ) by A35, XREAL_1:6;
then n + 1 in dom p by FINSEQ_3:25;
then A38: q . (n + 1) = p . (m + 1) by FINSEQ_1:def 7;
A39: q . n = p . m by FINSEQ_1:def 7;
the_Vertices_of the removeVertex of G,v c= the_Vertices_of G ;
then reconsider v1 = v1, v2 = v2 as Vertex of G by TARSKI:def 3;
take v1 ; :: thesis:
take v2 ; :: thesis:
take e ; :: thesis:
(the_Edges_of the removeVertex of G,v) \ (the_Edges_of (p . m)) c= (the_Edges_of G) \ (the_Edges_of (p . m)) by XBOOLE_1:33;
hence ( q . (n + 1) is addAdjVertex of q . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (q . n)) & ( ( v1 in the_Vertices_of (q . n) & not v2 in the_Vertices_of (q . n) ) or ( not v1 in the_Vertices_of (q . n) & v2 in the_Vertices_of (q . n) ) ) ) by A37, A38, A39; :: thesis:

end;

A40: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A5);
let G be _finite Tree-like _Graph; :: thesis:
let H be connected Subgraph of G; :: thesis:
(G .order()) - (H .order()) is Nat by GLIB_000:75, NAT_1:21;
hence ex p being non empty Graph-yielding _finite Tree-like FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .order()) - (H .order())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & ( ( v1 in the_Vertices_of (p . n) & not v2 in the_Vertices_of (p . n) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) ) ) ) by A40; :: thesis: