let T be _Tree; :: thesis: for a, b being Vertex of T
for t being _Subtree of T
for a', b' being Vertex of t st a = a' & b = b' holds
T .pathBetween a,b = t .pathBetween a',b'
let a, b be Vertex of T; :: thesis: for t being _Subtree of T
for a', b' being Vertex of t st a = a' & b = b' holds
T .pathBetween a,b = t .pathBetween a',b'
let t be _Subtree of T; :: thesis: for a', b' being Vertex of t st a = a' & b = b' holds
T .pathBetween a,b = t .pathBetween a',b'
let a', b' be Vertex of t; :: thesis: ( a = a' & b = b' implies T .pathBetween a,b = t .pathBetween a',b' )
assume that
A1: a = a' and
A2: b = b' ; :: thesis: T .pathBetween a,b = t .pathBetween a',b'
set tp = t .pathBetween a',b';
A3: t .pathBetween a',b' is_Walk_from a',b' by Def2;
reconsider tp' = t .pathBetween a',b' as Walk of T by GLIB_001:168;
A4: tp' is Path-like by GLIB_001:177;
A5: tp' .first() = (t .pathBetween a',b') .first()
.= a by A1, A3, GLIB_001:def 23 ;
tp' .last() = (t .pathBetween a',b') .last()
.= b by A2, A3, GLIB_001:def 23 ;
then tp' is_Walk_from a,b by A5, GLIB_001:def 23;
hence T .pathBetween a,b = t .pathBetween a',b' by A4, Def2; :: thesis: verum