let P be _finite non _trivial Path-like _Graph; :: thesis:
consider p being non empty Graph-yielding _finite Path-like FinSequence such that
A1: ( p . 1 is 2 -vertex & p . 1 is Path-like & p . (len p) = P & (len p) + 1 = P .order() ) and
A2: for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of P ex e being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & e in (the_Edges_of P) \ (the_Edges_of (p . n)) & ( ( v1 in Endvertices (p . n) & not v2 in the_Vertices_of (p . n) ) or ( not v1 in the_Vertices_of (p . n) & v2 in Endvertices (p . n) ) ) ) by Th25;
defpred S₁[ Nat] means for H being _Graph st H = p . ($1 + 1) & $1 <= (len p) - 1 holds
H .minDegree() = 1;
A3: S₁[ 0 ]

let H be _Graph; :: thesis:
assume ( H = p . (0 + 1) & 0 <= (len p) - 1 ) ; :: thesis:
then A4: ( H is 2 -vertex & H is Path-like ) by A1;

take v = the Vertex of H; :: thesis:
thus A6: v .degree() = 1 by A4, GLIB_000:174; :: thesis:
let w be Vertex of H; :: thesis:
thus v .degree() c= w .degree() by A4, A6, GLIB_000:174; :: thesis:

end;

hence H .minDegree() = 1 by GLIB_013:36; :: thesis:

end;

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

let k be Nat; :: thesis:
assume A8: S₁[k] ; :: thesis:
let H be _Graph; :: thesis:
assume A9: ( H = p . ((k + 1) + 1) & k + 1 <= (len p) - 1 ) ; :: thesis:
(len p) - 1 <= (len p) - 0 by XREAL_1:10;
then A10: k + 1 <= len p by A9, XXREAL_0:2;
0 + 1 <= k + 1 by XREAL_1:6;
then reconsider n = k + 1 as Element of dom p by A10, FINSEQ_3:25;
consider v1, v2 being Vertex of P, e being object such that
A11: H is addAdjVertex of p . n,v1,e,v2 and
A12: e in (the_Edges_of P) \ (the_Edges_of (p . n)) and
A13: ( ( v1 in Endvertices (p . n) & not v2 in the_Vertices_of (p . n) ) or ( not v1 in the_Vertices_of (p . n) & v2 in Endvertices (p . n) ) ) by A2, A9;
(k + 1) - 1 <= (len p) - 1 by A10, XREAL_1:9;
then A14: (p . n) .minDegree() = 1 by A8;
A15: not e in the_Edges_of (p . n) by A12, XBOOLE_0:def 5;

per cases by A13;

suppose A16: ( v1 in Endvertices (p . n) & not v2 in the_Vertices_of (p . n) ) ; :: thesis:

then reconsider v1 = v1 as Vertex of (p . n) ;

A17: the_Vertices_of H = (the_Vertices_of (p . n)) \/ {v2} by A11, A15, A16, GLIB_006:def 12;
v2 in {v2} by TARSKI:def 1;
then reconsider v2 = v2 as Vertex of H by A17, XBOOLE_0:def 3;
take v2 = v2; :: thesis:
thus A18: v2 .degree() = 1 by A11, A15, A16, GLIB_006:141, GLIB_000:174; :: thesis:
let w be Vertex of H; :: thesis:

suppose w = v2 ; :: thesis:

hence v2 .degree() c= w .degree() ; :: thesis:

end;

suppose w <> v2 ; :: thesis:

then not w in {v2} by TARSKI:def 1;
then reconsider u = w as Vertex of (p . n) by A17, XBOOLE_0:def 3;
A19: 1 c= u .degree() by A14, GLIB_013:35;
p . n is Subgraph of H by A11, GLIB_006:57;
then u .degree() c= w .degree() by Th1;
hence v2 .degree() c= w .degree() by A18, A19, XBOOLE_1:1; :: thesis:

end;

end;

end;

hence H .minDegree() = 1 by GLIB_013:36; :: thesis:

end;

suppose A20: ( not v1 in the_Vertices_of (p . n) & v2 in Endvertices (p . n) ) ; :: thesis:

then reconsider v2 = v2 as Vertex of (p . n) ;

A21: the_Vertices_of H = (the_Vertices_of (p . n)) \/ {v1} by A11, A15, A20, GLIB_006:def 12;
v1 in {v1} by TARSKI:def 1;
then reconsider v1 = v1 as Vertex of H by A21, XBOOLE_0:def 3;
take v1 = v1; :: thesis:
thus A22: v1 .degree() = 1 by A11, A15, A20, GLIB_006:142, GLIB_000:174; :: thesis:
let w be Vertex of H; :: thesis:

suppose w = v1 ; :: thesis:

hence v1 .degree() c= w .degree() ; :: thesis:

end;

suppose w <> v1 ; :: thesis:

then not w in {v1} by TARSKI:def 1;
then reconsider u = w as Vertex of (p . n) by A21, XBOOLE_0:def 3;
A23: 1 c= u .degree() by A14, GLIB_013:35;
p . n is Subgraph of H by A11, GLIB_006:57;
then u .degree() c= w .degree() by Th1;
hence v1 .degree() c= w .degree() by A22, A23, XBOOLE_1:1; :: thesis:

end;

end;

end;

hence H .minDegree() = 1 by GLIB_013:36; :: thesis:

end;

end;

end;

A24: for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A7);
0 < len p ;
then 0 + 1 < (len p) + 1 by XREAL_1:6;
then 1 <= len p by NAT_1:13;
then 1 - 1 <= (len p) - 1 by XREAL_1:9;
then ((len p) -' 1) + 1 = len p by NAT_D:72;
hence P .minDegree() = 1 by A1, A24; :: thesis: