let T be _Tree; :: thesis: for P being Path of T
for a, b being Vertex of T
for i, j being odd Nat st i <= j & j <= len P & P . i = a & P . j = b holds
T .pathBetween a,b = P .cut i,j
let P be Path of T; :: thesis: for a, b being Vertex of T
for i, j being odd Nat st i <= j & j <= len P & P . i = a & P . j = b holds
T .pathBetween a,b = P .cut i,j
let a, b be Vertex of T; :: thesis: for i, j being odd Nat st i <= j & j <= len P & P . i = a & P . j = b holds
T .pathBetween a,b = P .cut i,j
let i, j be odd Nat; :: thesis: ( i <= j & j <= len P & P . i = a & P . j = b implies T .pathBetween a,b = P .cut i,j )
assume A1: ( i <= j & j <= len P & P . i = a & P . j = b ) ; :: thesis: T .pathBetween a,b = P .cut i,j
reconsider i' = i, j' = j as odd Element of NAT by ORDINAL1:def 13;
P .cut i',j' is_Walk_from a,b by A1, GLIB_001:38;
hence T .pathBetween a,b = P .cut i,j by Def2; :: thesis: verum