let T be _Tree; for a, b, c being Vertex of T holds
( c in (T .pathBetween (a,b)) .vertices() iff ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} )
let a, b, c be Vertex of T; ( c in (T .pathBetween (a,b)) .vertices() iff ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} )
set Pac = T .pathBetween (a,c);
set Pcb = T .pathBetween (c,b);
set Pab = T .pathBetween (a,b);
A1: (T .pathBetween (a,c)) .last() =
c
by Th28
.=
(T .pathBetween (c,b)) .first()
by Th28
;
thus
( c in (T .pathBetween (a,b)) .vertices() implies ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} )
( ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} implies c in (T .pathBetween (a,b)) .vertices() )proof
assume A2:
c in (T .pathBetween (a,b)) .vertices()
;
((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c}
thus
((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) c= {c}
XBOOLE_0:def 10 {c} c= ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices())proof
let x be
object ;
TARSKI:def 3 ( not x in ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) or x in {c} )
assume A3:
x in ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices())
;
x in {c}
then A4:
x in (T .pathBetween (a,c)) .vertices()
by XBOOLE_0:def 4;
A5:
x in (T .pathBetween (c,b)) .vertices()
by A3, XBOOLE_0:def 4;
A6:
(T .pathBetween (c,b)) .first() = c
by Th28;
A7:
T .pathBetween (
a,
b)
= (T .pathBetween (a,c)) .append (T .pathBetween (c,b))
by A2, Th36;
A8:
(
(T .pathBetween (a,b)) .first() = a &
(T .pathBetween (a,b)) .last() = b )
by Th28;
A9:
(T .pathBetween (a,c)) .last() = c
by Th28;
per cases
( not T .pathBetween (a,b) is V5() or not T .pathBetween (a,b) is V5() )
;
suppose
T .pathBetween (
a,
b) is
V5()
;
x in {c}then
(T .pathBetween (a,b)) .first() = (T .pathBetween (a,b)) .last()
by GLIB_001:127;
then A10:
(T .pathBetween (a,b)) .vertices() = {a}
by A8, Th30;
x in ((T .pathBetween (a,c)) .vertices()) \/ ((T .pathBetween (c,b)) .vertices())
by A4, XBOOLE_0:def 3;
then
x in (T .pathBetween (a,b)) .vertices()
by A7, A9, A6, GLIB_001:93;
hence
x in {c}
by A2, A10, TARSKI:def 1;
verum end; suppose A11:
T .pathBetween (
a,
b) is
V5()
;
x in {c}consider n being
odd Element of
NAT such that A12:
n <= len (T .pathBetween (c,b))
and A13:
(T .pathBetween (c,b)) . n = x
by A5, GLIB_001:87;
1
<= n
by ABIAN:12;
then
1
- 1
<= n - 1
by XREAL_1:9;
then reconsider n1 =
n - 1 as
even Element of
NAT by INT_1:3;
consider m being
odd Element of
NAT such that A14:
m <= len (T .pathBetween (a,c))
and A15:
(T .pathBetween (a,c)) . m = x
by A4, GLIB_001:87;
A16:
m <= (len (T .pathBetween (a,c))) + n1
by A14, NAT_1:12;
1
<= m
by ABIAN:12;
then
m in dom (T .pathBetween (a,c))
by A14, FINSEQ_3:25;
then A17:
(T .pathBetween (a,b)) . m = x
by A7, A15, GLIB_001:32;
(len (T .pathBetween (a,c))) + (n1 + 1) <= (len (T .pathBetween (a,c))) + (len (T .pathBetween (c,b)))
by A12, XREAL_1:6;
then
(((len (T .pathBetween (a,c))) + n1) + 1) - 1
<= ((len (T .pathBetween (a,c))) + (len (T .pathBetween (c,b)))) - 1
by XREAL_1:9;
then A18:
(((len (T .pathBetween (a,c))) + n1) + 1) - 1
<= ((len (T .pathBetween (a,b))) + 1) - 1
by A7, A9, A6, GLIB_001:28;
A19:
n1 + 1
= n
;
then
n1 < len (T .pathBetween (c,b))
by A12, NAT_1:13;
then A20:
(T .pathBetween (a,b)) . ((len (T .pathBetween (a,c))) + n1) = x
by A7, A9, A6, A13, A19, GLIB_001:33;
per cases
( m < (len (T .pathBetween (a,c))) + n1 or m = (len (T .pathBetween (a,c))) + n1 )
by A16, XXREAL_0:1;
suppose A21:
m < (len (T .pathBetween (a,c))) + n1
;
x in {c}then (T .pathBetween (a,b)) .first() =
x
by A17, A20, A18, GLIB_001:def 28
.=
(T .pathBetween (a,b)) .last()
by A17, A20, A18, A21, GLIB_001:def 28
;
hence
x in {c}
by A11, GLIB_001:def 24;
verum end; end;
end;
let x be
object ;
TARSKI:def 3 ( not x in {c} or x in ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) )
assume
x in {c}
;
x in ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices())
then A23:
x = c
by TARSKI:def 1;
then
x = (T .pathBetween (c,b)) .first()
by Th28;
then A24:
x in (T .pathBetween (c,b)) .vertices()
by GLIB_001:88;
x = (T .pathBetween (a,c)) .last()
by A23, Th28;
then
x in (T .pathBetween (a,c)) .vertices()
by GLIB_001:88;
hence
x in ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices())
by A24, XBOOLE_0:def 4;
verum
end;
( (T .pathBetween (a,c)) .first() = a & (T .pathBetween (c,b)) .last() = b )
by Th28;
then A25:
(T .pathBetween (a,c)) .append (T .pathBetween (c,b)) is_Walk_from a,b
by A1, GLIB_001:30;
assume
((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c}
; c in (T .pathBetween (a,b)) .vertices()
then
((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {((T .pathBetween (a,c)) .last())}
by Th28;
then
(T .pathBetween (a,c)) .append (T .pathBetween (c,b)) is Path-like
by A1, Th38;
then
T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b))
by A25, Def2;
hence
c in (T .pathBetween (a,b)) .vertices()
by Th36; verum