defpred S₁[ Nat] means for T being _finite non _trivial _Tree
for v being Vertex of T st T .order() = $1 + 2 holds
ex v1, v2 being Vertex of T st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v in (T .pathBetween (v1,v2)) .vertices() );
A1: S₁[ 0 ]

let T be _finite non _trivial _Tree; :: thesis:
let v be Vertex of T; :: thesis:
assume A2: T .order() = 0 + 2 ; :: thesis:
then card (the_Vertices_of T) = 2 by GLIB_000:def 24;
then consider v1, v2 being object such that
A3: ( v1 <> v2 & the_Vertices_of T = {v1,v2} ) by CARD_2:60;
reconsider v1 = v1, v2 = v2 as Vertex of T by A3, TARSKI:def 2;
take v1 ; :: thesis:
take v2 ; :: thesis:
thus v1 <> v2 by A3; :: thesis:
thus ( v1 is endvertex & v2 is endvertex ) by A2, Th27; :: thesis:
( v = v1 or v = v2 ) by A3, TARSKI:def 2;
hence v in (T .pathBetween (v1,v2)) .vertices() by HELLY:29; :: thesis:

end;

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

proof

let k be Nat; :: thesis:
assume A5: S₁[k] ; :: thesis:
let T be _finite non _trivial _Tree; :: thesis:
let v be Vertex of T; :: thesis:
assume A6: T .order() = (k + 1) + 2 ; :: thesis:
set v0 = the endvertex Vertex of T;

per cases ;

suppose A7: v = the endvertex Vertex of T ; :: thesis:

consider v1, v2 being Vertex of T such that
A8: ( v1 <> v2 & v1 is endvertex & v2 is endvertex ) by GLIB_002:45;

per cases ;

suppose A9: v <> v1 ; :: thesis:

take v ; :: thesis:
take v1 ; :: thesis:
thus ( v <> v1 & v is endvertex & v1 is endvertex ) by A7, A8, A9; :: thesis:
thus v in (T .pathBetween (v,v1)) .vertices() by HELLY:29; :: thesis:

end;

suppose A10: v = v1 ; :: thesis:

take v ; :: thesis:
take v2 ; :: thesis:
thus ( v <> v2 & v is endvertex & v2 is endvertex ) by A8, A10; :: thesis:
thus v in (T .pathBetween (v,v2)) .vertices() by HELLY:29; :: thesis:

end;

suppose A11: v <> the endvertex Vertex of T ; :: thesis:

set T0 = the removeVertex of T, the endvertex Vertex of T;
a12: ( the removeVertex of T, the endvertex Vertex of T .order()) + 1 = (k + 2) + 1 by A6, GLIB_000:48;
the removeVertex of T, the endvertex Vertex of T .order() <> 1

proof

assume the removeVertex of T, the endvertex Vertex of T .order() = 1 ; :: thesis:
then 0 + 1 = (k + 1) + 1 by a12;
hence contradiction ; :: thesis:

end;

proof

assume A21: w1 <> the endvertex Vertex of T .adj e0 ; :: thesis:
A22: v1 .edgesInOut() c= w1 .edgesInOut() by GLIB_000:78;
for e being object st e in w1 .edgesInOut() holds
e in v1 .edgesInOut()

proof

let e be object ; :: thesis:
assume A23: e in w1 .edgesInOut() ; :: thesis:
e <> e0

proof

assume e = e0 ; :: thesis:
then A24: e0 Joins w1,w1 .adj e0,T by A23, GLIB_000:67;
e0 in the endvertex Vertex of T .edgesInOut() by A15, TARSKI:def 1;
then e0 Joins the endvertex Vertex of T, the endvertex Vertex of T .adj e0,T by GLIB_000:67;
then ( w1 = the endvertex Vertex of T or w1 = the endvertex Vertex of T .adj e0 ) by A24, GLIB_000:15;
hence contradiction by A19, A21; :: thesis:

end;

then not e in {e0} by TARSKI:def 1;
then A25: e in the_Edges_of T0 by A16, A23, XBOOLE_0:def 5;
then ( (the_Source_of T0) . e = (the_Source_of T) . e & (the_Target_of T0) . e = (the_Target_of T) . e ) by GLIB_000:def 32;
then ( (the_Source_of T0) . e = w1 or (the_Target_of T0) . e = w1 ) by A23, GLIB_000:61;
hence e in v1 .edgesInOut() by A25, GLIB_000:61; :: thesis:

end;

then w1 .edgesInOut() c= v1 .edgesInOut() by TARSKI:def 3;
then v1 .edgesInOut() = w1 .edgesInOut() by A22, XBOOLE_0:def 10;
hence w1 is endvertex by A17, GLIB_000:18, GLIB_000:def 51; :: thesis:

end;

A26: ( w2 <> the endvertex Vertex of T .adj e0 implies w2 is endvertex )

proof

assume A27: w2 <> the endvertex Vertex of T .adj e0 ; :: thesis:
A28: v2 .edgesInOut() c= w2 .edgesInOut() by GLIB_000:78;
for e being object st e in w2 .edgesInOut() holds
e in v2 .edgesInOut()

proof

let e be object ; :: thesis:
assume A29: e in w2 .edgesInOut() ; :: thesis:
e <> e0

proof

assume e = e0 ; :: thesis:
then A30: e0 Joins w2,w2 .adj e0,T by A29, GLIB_000:67;
e0 in the endvertex Vertex of T .edgesInOut() by A15, TARSKI:def 1;
then e0 Joins the endvertex Vertex of T, the endvertex Vertex of T .adj e0,T by GLIB_000:67;
then ( w2 = the endvertex Vertex of T or w2 = the endvertex Vertex of T .adj e0 ) by A30, GLIB_000:15;
hence contradiction by A19, A27; :: thesis:

end;

then not e in {e0} by TARSKI:def 1;
then A31: e in the_Edges_of T0 by A16, A29, XBOOLE_0:def 5;
then ( (the_Source_of T0) . e = (the_Source_of T) . e & (the_Target_of T0) . e = (the_Target_of T) . e ) by GLIB_000:def 32;
then ( (the_Source_of T0) . e = w2 or (the_Target_of T0) . e = w2 ) by A29, GLIB_000:61;
hence e in v2 .edgesInOut() by A31, GLIB_000:61; :: thesis:

end;

then w2 .edgesInOut() c= v2 .edgesInOut() by TARSKI:def 3;
then v2 .edgesInOut() = w2 .edgesInOut() by A28, XBOOLE_0:def 10;
hence w2 is endvertex by A18, GLIB_000:18, GLIB_000:def 51; :: thesis:

end;

A32: T0 .pathBetween (v1,v2) = T .pathBetween (w1,w2) by HELLY:33;

per cases ;

suppose A33: w1 = the endvertex Vertex of T .adj e0 ; :: thesis:

proof

let x be object ; :: thesis:

hereby :: thesis:

assume x in ((T .pathBetween ( the endvertex Vertex of T,w1)) .vertices()) /\ ((T .pathBetween (w1,w2)) .vertices()) ; :: thesis:
then A38: ( x in (T .pathBetween ( the endvertex Vertex of T,w1)) .vertices() & x in (T .pathBetween (w1,w2)) .vertices() ) by XBOOLE_0:def 4;
then A39: x in { the endvertex Vertex of T,w1} by A35, A36, GLIB_001:91;
x in (T0 .pathBetween (v1,v2)) .vertices() by A32, A38, GLIB_001:98;
then x in the_Vertices_of T0 ;
hence x = w1 by A19, A39, TARSKI:def 2; :: thesis:

end;

assume x = w1 ; :: thesis:
then ( x = (T .pathBetween ( the endvertex Vertex of T,w1)) .last() & x = (T .pathBetween (w1,w2)) .first() ) by HELLY:28;
then ( x in (T .pathBetween ( the endvertex Vertex of T,w1)) .vertices() & x in (T .pathBetween (w1,w2)) .vertices() ) by GLIB_001:88;
hence x in ((T .pathBetween ( the endvertex Vertex of T,w1)) .vertices()) /\ ((T .pathBetween (w1,w2)) .vertices()) by XBOOLE_0:def 4; :: thesis:

end;

end;

suppose A41: w2 = the endvertex Vertex of T .adj e0 ; :: thesis:

proof

let x be object ; :: thesis:

hereby :: thesis:

assume x in ((T .pathBetween (w1,w2)) .vertices()) /\ ((T .pathBetween (w2, the endvertex Vertex of T)) .vertices()) ; :: thesis:
then A46: ( x in (T .pathBetween (w1,w2)) .vertices() & x in (T .pathBetween (w2, the endvertex Vertex of T)) .vertices() ) by XBOOLE_0:def 4;
then A47: x in {w2, the endvertex Vertex of T} by A43, A44, GLIB_001:91;
x in (T0 .pathBetween (v1,v2)) .vertices() by A32, A46, GLIB_001:98;
then x in the_Vertices_of T0 ;
hence x = w2 by A19, A47, TARSKI:def 2; :: thesis:

end;

assume x = w2 ; :: thesis:
then ( x in (T .pathBetween (w1,w2)) .vertices() & x in (T .pathBetween (w2, the endvertex Vertex of T)) .vertices() ) by GLIB_001:88, A45;
hence x in ((T .pathBetween (w1,w2)) .vertices()) /\ ((T .pathBetween (w2, the endvertex Vertex of T)) .vertices()) by XBOOLE_0:def 4; :: thesis:

end;

then ((T .pathBetween (w1,w2)) .vertices()) /\ ((T .pathBetween (w2, the endvertex Vertex of T)) .vertices()) = {((T .pathBetween (w1,w2)) .last())} by A45, TARSKI:def 1;
then reconsider P = (T .pathBetween (w1,w2)) .append (T .pathBetween (w2, the endvertex Vertex of T)) as Path of T by A45, HELLY:38;
( T .pathBetween (w1,w2) is_Walk_from w1,w2 & T .pathBetween (w2, the endvertex Vertex of T) is_Walk_from w2, the endvertex Vertex of T ) by HELLY:def 2;
then A48: P = T .pathBetween (w1, the endvertex Vertex of T) by GLIB_001:31, HELLY:def 2;
(T0 .pathBetween (v1,v2)) .vertices() = (T .pathBetween (w1,w2)) .vertices() by HELLY:33, GLIB_001:98;
then v in ((T .pathBetween (w1,w2)) .vertices()) \/ ((T .pathBetween (w2, the endvertex Vertex of T)) .vertices()) by A14, XBOOLE_0:def 3;
hence v in (T .pathBetween (w1, the endvertex Vertex of T)) .vertices() by A45, A48, GLIB_001:93; :: thesis:

end;

suppose A49: ( w1 <> the endvertex Vertex of T .adj e0 & w2 <> the endvertex Vertex of T .adj e0 ) ; :: thesis:

take w1 ; :: thesis:
take w2 ; :: thesis:
thus ( w1 <> w2 & w1 is endvertex & w2 is endvertex ) by A13, A20, A26, A49; :: thesis:
thus v in (T .pathBetween (w1,w2)) .vertices() by A14, GLIB_001:98, HELLY:33; :: thesis:

end;

A50: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A4);
let T be _finite non _trivial _Tree; :: thesis:
let v be Vertex of T; :: thesis:
( T .order() >= 1 & T .order() <> 1 ) by GLIB_000:25, GLIB_000:26;
then T .order() > 1 by XXREAL_0:1;
then T .order() >= 1 + 1 by INT_1:7;
then consider k being Nat such that
A51: T .order() = 2 + k by NAT_1:10;
thus ex v1, v2 being Vertex of T st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v in (T .pathBetween (v1,v2)) .vertices() ) by A50, A51; :: thesis: