defpred S₁[ Nat] means for G being _finite Path-like _Graph
for H being connected Subgraph of G st $1 = (G .order()) - (H .order()) holds
ex p being non empty Graph-yielding _finite Path-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) & ( not p . n is _trivial implies v1 in Endvertices (p . n) ) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) & ( not p . n is _trivial implies v2 in Endvertices (p . n) ) ) ) ) ) );
A1: S₁[ 0 ]

proof

let G be _finite Path-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 GLIB_008:21;
reconsider p = <*G*> as non empty Graph-yielding _finite Path-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) & ( not p . n is _trivial implies v1 in Endvertices (p . n) ) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) & ( not p . n is _trivial implies v2 in Endvertices (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 Path-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() by A7;
then A9: not H is spanning by GLIB_000:117;
G .order() <> 1 by A8;
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, GLIB_008:31;
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;

A19: the removeVertex of G,v is connected by A10, A11;
then consider p being non empty Graph-yielding _finite Path-like FinSequence such that
A20: ( p . 1 == H & p . (len p) = the removeVertex of G,v & len p = (( the removeVertex of G,v .order()) - (H .order())) + 1 ) and
A21: 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) & ( not p . n is _trivial implies v1 in Endvertices (p . n) ) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) & ( not p . n is _trivial implies v2 in Endvertices (p . n) ) ) ) ) by A6, A14, A16;
reconsider q = p ^ <*G*> as non empty Graph-yielding _finite Path-like FinSequence ;
take q ; :: thesis:
1 <= len p by FINSEQ_1:20;
then 1 in dom p by FINSEQ_3:25;
hence q . 1 == H by A20, FINSEQ_1:def 7; :: thesis:
A22: len q = (len p) + (len <*G*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:40 ;
hence A23: q . (len q) = G by FINSEQ_1:42; :: thesis:
thus len q = ((G .order()) - (H .order())) + 1 by A13, A20, A22; :: thesis:
let n be Element of dom q; :: thesis:
assume n <= (len q) - 1 ; :: thesis:

per cases by Lm4;

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

then A25: q . (n + 1) = G by A23;
A26: 1 <= n by FINSEQ_3:25;
A27: n = len p by A22, A24;
then n in dom p by A26, FINSEQ_3:25;
then A28: q . n = the removeVertex of G,v by A20, A27, FINSEQ_1:def 7;
A29: e0 in v .edgesInOut() by A12, TARSKI:def 1;
then A30: e0 in the_Edges_of G ;
e0 in {e0} by TARSKI:def 1;
then A31: not e0 in the_Edges_of (q . n) by A15, A28, 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 A32: not v in the_Vertices_of (q . n) by A10, A28, GLIB_000:47;
v .adj e0 <> v by A12, A29, 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 A33: v .adj e0 in the_Vertices_of (q . n) by A10, A28, GLIB_000:47;

per cases by A10, A12, GLIB_008:38;

suppose A34: 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 A25, A28, A34; :: thesis:
( not q . n is _trivial implies v .adj e0 in Endvertices (q . n) )

proof

assume not q . n is _trivial ; :: thesis:
then A35: not the removeVertex of G,v is _trivial by A28;
A36: the removeVertex of G,v is Path-like by A11, Th21;
reconsider w = v .adj e0 as Vertex of the removeVertex of G,v by A28, A33;
w .degree() in succ 2 by A36, ORDINAL1:22;
then A37: w .degree() in {0,1,2} by CARD_1:51;
A38: not w .degree() = 2

proof

assume A39: w .degree() = 2 ; :: thesis:
(v .adj e0) .degree() = (w .degree()) +` 1 by A28, A31, A32, A34, Th10
.= 2 + 1 by A39 ;
then succ 2 c= 2 by Def1;
then 2 in 2 by ORDINAL1:21;
hence contradiction ; :: thesis:

end;

not w .degree() = 0 by A19, A35, GLIB_000:157;
then w .degree() = 1 by A37, A38, ENUMSET1:def 1;
hence v .adj e0 in Endvertices (q . n) by A28, GLIB_006:56, GLIB_000:174; :: thesis:

end;

hence ( 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) & ( not q . n is _trivial implies v .adj e0 in Endvertices (q . n) ) ) or ( not v .adj e0 in the_Vertices_of (q . n) & v in the_Vertices_of (q . n) & ( not q . n is _trivial implies v in Endvertices (q . n) ) ) ) ) by A30, A31, A32, A33, XBOOLE_0:def 5; :: thesis:

end;

suppose A40: 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 A25, A28, A40; :: thesis:
( not q . n is _trivial implies v .adj e0 in Endvertices (q . n) )

proof

assume not q . n is _trivial ; :: thesis:
then A41: not the removeVertex of G,v is _trivial by A28;
A42: the removeVertex of G,v is Path-like by A11, Th21;
reconsider w = v .adj e0 as Vertex of the removeVertex of G,v by A28, A33;
w .degree() in succ 2 by A42, ORDINAL1:22;
then A43: w .degree() in {0,1,2} by CARD_1:51;
A44: not w .degree() = 2

proof

assume A45: w .degree() = 2 ; :: thesis:
(v .adj e0) .degree() = (w .degree()) +` 1 by A28, A31, A32, A40, Th11
.= 2 + 1 by A45 ;
then succ 2 c= 2 by Def1;
then 2 in 2 by ORDINAL1:21;
hence contradiction ; :: thesis:

end;

not w .degree() = 0 by A19, A41, GLIB_000:157;
then w .degree() = 1 by A43, A44, ENUMSET1:def 1;
hence v .adj e0 in Endvertices (q . n) by A28, GLIB_006:56, GLIB_000:174; :: thesis:

end;

hence ( 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) & ( not q . n is _trivial implies v in Endvertices (q . n) ) ) or ( not v in the_Vertices_of (q . n) & v .adj e0 in the_Vertices_of (q . n) & ( not q . n is _trivial implies v .adj e0 in Endvertices (q . n) ) ) ) ) by A30, A31, A32, A33, XBOOLE_0:def 5; :: thesis:

end;

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

then A47: 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 A47, FINSEQ_3:25;
consider v1, v2 being Vertex of the removeVertex of G,v, e being object such that
A48: ( 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) & ( not p . m is _trivial implies v1 in Endvertices (p . m) ) ) or ( not v1 in the_Vertices_of (p . m) & v2 in the_Vertices_of (p . m) & ( not p . m is _trivial implies v2 in Endvertices (p . m) ) ) ) ) by A21, A46;
( 1 + 0 <= n + 1 & n + 1 <= ((len p) - 1) + 1 ) by A46, XREAL_1:6;
then n + 1 in dom p by FINSEQ_3:25;
then A49: q . (n + 1) = p . (m + 1) by FINSEQ_1:def 7;
A50: 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) & ( not q . n is _trivial implies v1 in Endvertices (q . n) ) ) or ( not v1 in the_Vertices_of (q . n) & v2 in the_Vertices_of (q . n) & ( not q . n is _trivial implies v2 in Endvertices (q . n) ) ) ) ) by A48, A49, A50; :: thesis:

end;

A51: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A5);
let G be _finite Path-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 Path-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) & ( not p . n is _trivial implies v1 in Endvertices (p . n) ) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) & ( not p . n is _trivial implies v2 in Endvertices (p . n) ) ) ) ) ) ) by A51; :: thesis: