let T be _Tree; :: thesis: 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; :: thesis: ( 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} ) :: thesis: ( ((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() ; :: thesis: ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c}
thus ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) c= {c} :: according to XBOOLE_0:def 10 :: thesis: {c} c= ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices())

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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()) ; :: thesis: 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 trivial or not T .pathBetween (a,b) is trivial ) ;

suppose T .pathBetween (a,b) is trivial ; :: thesis: 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; :: thesis: verum

end;

suppose A11: T .pathBetween (a,b) is trivial ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum

end;

suppose A22: m = (len (T .pathBetween (a,c))) + n1 ; :: thesis: x in {c}

then n1 = 0 by A14, NAT_1:16;
hence x in {c} by A9, A15, A22, TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {c} or x in ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) )
assume x in {c} ; :: thesis: 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; :: thesis: 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} ; :: thesis: 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; :: thesis: verum