defpred S1[ 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:
S1[ 0 ]
proof
let T be
_finite non
_trivial _Tree;
for v being Vertex of T st T .order() = 0 + 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() )let v be
Vertex of
T;
( T .order() = 0 + 2 implies ex v1, v2 being Vertex of T st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v in (T .pathBetween (v1,v2)) .vertices() ) )
assume A2:
T .order() = 0 + 2
;
ex v1, v2 being Vertex of T st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v in (T .pathBetween (v1,v2)) .vertices() )
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
;
ex v2 being Vertex of T st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v in (T .pathBetween (v1,v2)) .vertices() )
take
v2
;
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v in (T .pathBetween (v1,v2)) .vertices() )
thus
v1 <> v2
by A3;
( v1 is endvertex & v2 is endvertex & v in (T .pathBetween (v1,v2)) .vertices() )
thus
(
v1 is
endvertex &
v2 is
endvertex )
by A2, Th27;
v in (T .pathBetween (v1,v2)) .vertices()
(
v = v1 or
v = v2 )
by A3, TARSKI:def 2;
hence
v in (T .pathBetween (v1,v2)) .vertices()
by HELLY:29;
verum
end;
A4:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A5:
S1[
k]
;
S1[k + 1]
let T be
_finite non
_trivial _Tree;
for v being Vertex of T st T .order() = (k + 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() )let v be
Vertex of
T;
( T .order() = (k + 1) + 2 implies ex v1, v2 being Vertex of T st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v in (T .pathBetween (v1,v2)) .vertices() ) )
assume A6:
T .order() = (k + 1) + 2
;
ex v1, v2 being Vertex of T st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v in (T .pathBetween (v1,v2)) .vertices() )
set v0 = the
endvertex Vertex of
T;
per cases
( v = the endvertex Vertex of T or v <> the endvertex Vertex of T )
;
suppose A11:
v <> the
endvertex Vertex of
T
;
ex v1, v2 being Vertex of T st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v in (T .pathBetween (v1,v2)) .vertices() )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
then reconsider T0 = the
removeVertex of
T, the
endvertex Vertex of
T as
_finite non
_trivial _Tree by GLIB_000:26;
not
v in { the endvertex Vertex of T}
by A11, TARSKI:def 1;
then
v in (the_Vertices_of T) \ { the endvertex Vertex of T}
by XBOOLE_0:def 5;
then
v in the_Vertices_of T0
by GLIB_000:47;
then consider v1,
v2 being
Vertex of
T0 such that A13:
(
v1 <> v2 &
v1 is
endvertex &
v2 is
endvertex )
and A14:
v in (T0 .pathBetween (v1,v2)) .vertices()
by A5, a12;
the_Vertices_of T0 c= the_Vertices_of T
by GLIB_000:def 32;
then reconsider w1 =
v1,
w2 =
v2 as
Vertex of
T by TARSKI:def 3;
consider e0 being
object such that A15:
( the
endvertex Vertex of
T .edgesInOut() = {e0} & not
e0 Joins the
endvertex Vertex of
T, the
endvertex Vertex of
T,
T )
by GLIB_000:def 51;
A16:
the_Edges_of T0 =
T .edgesBetween ((the_Vertices_of T) \ { the endvertex Vertex of T})
by GLIB_000:47
.=
(T .edgesBetween (the_Vertices_of T)) \ ( the endvertex Vertex of T .edgesInOut())
by Th1
.=
(the_Edges_of T) \ {e0}
by A15, GLIB_000:34
;
consider e1 being
object such that A17:
(
v1 .edgesInOut() = {e1} & not
e1 Joins v1,
v1,
T0 )
by A13, GLIB_000:def 51;
consider e2 being
object such that A18:
(
v2 .edgesInOut() = {e2} & not
e2 Joins v2,
v2,
T0 )
by A13, GLIB_000:def 51;
the
endvertex Vertex of
T in { the endvertex Vertex of T}
by TARSKI:def 1;
then
not the
endvertex Vertex of
T in (the_Vertices_of T) \ { the endvertex Vertex of T}
by XBOOLE_0:def 5;
then A19:
not the
endvertex Vertex of
T in the_Vertices_of T0
by GLIB_000:47;
A20:
(
w1 <> the
endvertex Vertex of
T .adj e0 implies
w1 is
endvertex )
A26:
(
w2 <> the
endvertex Vertex of
T .adj e0 implies
w2 is
endvertex )
A32:
T0 .pathBetween (
v1,
v2)
= T .pathBetween (
w1,
w2)
by HELLY:33;
per cases
( w1 = the endvertex Vertex of T .adj e0 or w2 = the endvertex Vertex of T .adj e0 or ( w1 <> the endvertex Vertex of T .adj e0 & w2 <> the endvertex Vertex of T .adj e0 ) )
;
suppose A33:
w1 = the
endvertex Vertex of
T .adj e0
;
ex v1, v2 being Vertex of T st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v in (T .pathBetween (v1,v2)) .vertices() )then A34:
w2 <> the
endvertex Vertex of
T .adj e0
by A13;
take
the
endvertex Vertex of
T
;
ex v2 being Vertex of T st
( the endvertex Vertex of T <> v2 & the endvertex Vertex of T is endvertex & v2 is endvertex & v in (T .pathBetween ( the endvertex Vertex of T,v2)) .vertices() )take
w2
;
( the endvertex Vertex of T <> w2 & the endvertex Vertex of T is endvertex & w2 is endvertex & v in (T .pathBetween ( the endvertex Vertex of T,w2)) .vertices() )thus
( the
endvertex Vertex of
T <> w2 & the
endvertex Vertex of
T is
endvertex &
w2 is
endvertex )
by A19, A26, A34;
v in (T .pathBetween ( the endvertex Vertex of T,w2)) .vertices()
e0 in the
endvertex Vertex of
T .edgesInOut()
by A15, TARSKI:def 1;
then A35:
e0 Joins the
endvertex Vertex of
T,
w1,
T
by A33, GLIB_000:67;
then A36:
T .walkOf ( the
endvertex Vertex of
T,
e0,
w1)
= T .pathBetween ( the
endvertex Vertex of
T,
w1)
by Th29;
set P1 =
T .pathBetween ( the
endvertex Vertex of
T,
w1);
set P2 =
T .pathBetween (
w1,
w2);
set P =
(T .pathBetween ( the endvertex Vertex of T,w1)) .append (T .pathBetween (w1,w2));
A37:
(
(T .pathBetween ( the endvertex Vertex of T,w1)) .last() = w1 &
(T .pathBetween (w1,w2)) .first() = w1 )
by HELLY:28;
for
x being
object holds
(
x in ((T .pathBetween ( the endvertex Vertex of T,w1)) .vertices()) /\ ((T .pathBetween (w1,w2)) .vertices()) iff
x = w1 )
proof
let x be
object ;
( x in ((T .pathBetween ( the endvertex Vertex of T,w1)) .vertices()) /\ ((T .pathBetween (w1,w2)) .vertices()) iff x = w1 )
hereby ( x = w1 implies x in ((T .pathBetween ( the endvertex Vertex of T,w1)) .vertices()) /\ ((T .pathBetween (w1,w2)) .vertices()) )
assume
x in ((T .pathBetween ( the endvertex Vertex of T,w1)) .vertices()) /\ ((T .pathBetween (w1,w2)) .vertices())
;
x = w1then 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;
verum
end;
assume
x = w1
;
x in ((T .pathBetween ( the endvertex Vertex of T,w1)) .vertices()) /\ ((T .pathBetween (w1,w2)) .vertices())
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;
verum
end; then
((T .pathBetween ( the endvertex Vertex of T,w1)) .vertices()) /\ ((T .pathBetween (w1,w2)) .vertices()) = {((T .pathBetween ( the endvertex Vertex of T,w1)) .last())}
by A37, TARSKI:def 1;
then reconsider P =
(T .pathBetween ( the endvertex Vertex of T,w1)) .append (T .pathBetween (w1,w2)) as
Path of
T by A37, HELLY:38;
(
T .pathBetween ( the
endvertex Vertex of
T,
w1)
is_Walk_from the
endvertex Vertex of
T,
w1 &
T .pathBetween (
w1,
w2)
is_Walk_from w1,
w2 )
by HELLY:def 2;
then A40:
P = T .pathBetween ( the
endvertex Vertex of
T,
w2)
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 ( the endvertex Vertex of T,w1)) .vertices()) \/ ((T .pathBetween (w1,w2)) .vertices())
by A14, XBOOLE_0:def 3;
hence
v in (T .pathBetween ( the endvertex Vertex of T,w2)) .vertices()
by A37, A40, GLIB_001:93;
verum end; suppose A41:
w2 = the
endvertex Vertex of
T .adj e0
;
ex v1, v2 being Vertex of T st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v in (T .pathBetween (v1,v2)) .vertices() )then A42:
w1 <> the
endvertex Vertex of
T .adj e0
by A13;
take
w1
;
ex v2 being Vertex of T st
( w1 <> v2 & w1 is endvertex & v2 is endvertex & v in (T .pathBetween (w1,v2)) .vertices() )take
the
endvertex Vertex of
T
;
( w1 <> the endvertex Vertex of T & w1 is endvertex & the endvertex Vertex of T is endvertex & v in (T .pathBetween (w1, the endvertex Vertex of T)) .vertices() )thus
(
w1 <> the
endvertex Vertex of
T &
w1 is
endvertex & the
endvertex Vertex of
T is
endvertex )
by A19, A20, A42;
v in (T .pathBetween (w1, the endvertex Vertex of T)) .vertices()
e0 in the
endvertex Vertex of
T .edgesInOut()
by A15, TARSKI:def 1;
then A43:
e0 Joins w2, the
endvertex Vertex of
T,
T
by A41, GLIB_000:67, GLIB_000:14;
then A44:
T .walkOf (
w2,
e0, the
endvertex Vertex of
T)
= T .pathBetween (
w2, the
endvertex Vertex of
T)
by Th29;
set P1 =
T .pathBetween (
w1,
w2);
set P2 =
T .pathBetween (
w2, the
endvertex Vertex of
T);
set P =
(T .pathBetween (w1,w2)) .append (T .pathBetween (w2, the endvertex Vertex of T));
A45:
(
(T .pathBetween (w1,w2)) .last() = w2 &
(T .pathBetween (w2, the endvertex Vertex of T)) .first() = w2 )
by HELLY:28;
for
x being
object holds
(
x in ((T .pathBetween (w1,w2)) .vertices()) /\ ((T .pathBetween (w2, the endvertex Vertex of T)) .vertices()) iff
x = w2 )
proof
let x be
object ;
( x in ((T .pathBetween (w1,w2)) .vertices()) /\ ((T .pathBetween (w2, the endvertex Vertex of T)) .vertices()) iff x = w2 )
hereby ( x = w2 implies x in ((T .pathBetween (w1,w2)) .vertices()) /\ ((T .pathBetween (w2, the endvertex Vertex of T)) .vertices()) )
assume
x in ((T .pathBetween (w1,w2)) .vertices()) /\ ((T .pathBetween (w2, the endvertex Vertex of T)) .vertices())
;
x = w2then 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;
verum
end;
assume
x = w2
;
x in ((T .pathBetween (w1,w2)) .vertices()) /\ ((T .pathBetween (w2, the endvertex Vertex of T)) .vertices())
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;
verum
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;
verum end; end;
end;
A50:
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A4);
let T be _finite non _trivial _Tree; for v being Vertex of T ex v1, v2 being Vertex of T st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v in (T .pathBetween (v1,v2)) .vertices() )
let v be Vertex of T; ex v1, v2 being Vertex of T st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v in (T .pathBetween (v1,v2)) .vertices() )
( 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; verum