let T be _Tree; for a, b, c being Vertex of T holds
( c in (T .pathBetween (a,b)) .vertices() iff T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) )
let a, b, c be Vertex of T; ( c in (T .pathBetween (a,b)) .vertices() iff T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) )
set P = T .pathBetween (a,b);
set ci = (T .pathBetween (a,b)) .find c;
set pac = T .pathBetween (a,c);
set pcb = T .pathBetween (c,b);
hereby ( T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) implies c in (T .pathBetween (a,b)) .vertices() )
A1:
T .pathBetween (
a,
b)
= (T .pathBetween (a,b)) .cut (1,
(len (T .pathBetween (a,b))))
by GLIB_001:39;
A2:
( 1
<= (T .pathBetween (a,b)) .find c & 1
= (2 * 0) + 1 )
by ABIAN:12;
assume A3:
c in (T .pathBetween (a,b)) .vertices()
;
T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b))then A4:
(T .pathBetween (a,b)) .find c <= len (T .pathBetween (a,b))
by GLIB_001:def 19;
A5:
(T .pathBetween (a,b)) . ((T .pathBetween (a,b)) .find c) = c
by A3, GLIB_001:def 19;
(T .pathBetween (a,b)) . (len (T .pathBetween (a,b))) =
(T .pathBetween (a,b)) .last()
.=
b
by Th28
;
then A6:
T .pathBetween (
c,
b)
= (T .pathBetween (a,b)) .cut (
((T .pathBetween (a,b)) .find c),
(len (T .pathBetween (a,b))))
by A4, A5, Th35;
(T .pathBetween (a,b)) . 1 =
(T .pathBetween (a,b)) .first()
.=
a
by Th28
;
then
T .pathBetween (
a,
c)
= (T .pathBetween (a,b)) .cut (1,
((T .pathBetween (a,b)) .find c))
by A4, A2, A5, Th35;
hence
T .pathBetween (
a,
b)
= (T .pathBetween (a,c)) .append (T .pathBetween (c,b))
by A4, A2, A6, A1, GLIB_001:38;
verum
end;
assume
T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b))
; c in (T .pathBetween (a,b)) .vertices()
then A7:
(T .pathBetween (a,c)) .vertices() c= (T .pathBetween (a,b)) .vertices()
by Th13, Th15;
c in (T .pathBetween (a,c)) .vertices()
by Th29;
hence
c in (T .pathBetween (a,b)) .vertices()
by A7; verum