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 set ; :: 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 ( 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:128;
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:94;
hence x in {c} by A2, A10, TARSKI:def 1; :: thesis: verum

end;

suppose A11: not 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:88;
1 <= n by ABIAN:12;
then 1 - 1 <= n - 1 by XREAL_1:11;
then reconsider n1 = n - 1 as even Element of NAT by INT_1:16;
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:88;
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:27;
then A17: (T .pathBetween a,b) . m = x by A7, A15, GLIB_001:33;
(len (T .pathBetween a,c)) + (n1 + 1) <= (len (T .pathBetween a,c)) + (len (T .pathBetween c,b)) by A12, XREAL_1:8;
then (((len (T .pathBetween a,c)) + n1) + 1) - 1 <= ((len (T .pathBetween a,c)) + (len (T .pathBetween c,b))) - 1 by XREAL_1:11;
then A18: (((len (T .pathBetween a,c)) + n1) + 1) - 1 <= ((len (T .pathBetween a,b)) + 1) - 1 by A7, A9, A6, GLIB_001:29;
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:34;

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 set ; :: 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:89;
x = (T .pathBetween a,c) .last() by A23, Th28;
then x in (T .pathBetween a,c) .vertices() by GLIB_001:89;
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:31;
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