let T be _Tree; :: thesis: for a being Vertex of T holds (T .pathBetween (a,a)) .vertices() = {a}

let a be Vertex of T; :: thesis: (T .pathBetween (a,a)) .vertices() = {a}

set P = T .pathBetween (a,a);

consider v being Vertex of T such that

A1: T .pathBetween (a,a) = T .walkOf v by GLIB_001:128;

( a = (T .pathBetween (a,a)) .first() & (T .walkOf v) .first() = v ) by Th28, GLIB_001:13;

hence (T .pathBetween (a,a)) .vertices() = {a} by A1, GLIB_001:90; :: thesis: verum

let a be Vertex of T; :: thesis: (T .pathBetween (a,a)) .vertices() = {a}

set P = T .pathBetween (a,a);

consider v being Vertex of T such that

A1: T .pathBetween (a,a) = T .walkOf v by GLIB_001:128;

( a = (T .pathBetween (a,a)) .first() & (T .walkOf v) .first() = v ) by Th28, GLIB_001:13;

hence (T .pathBetween (a,a)) .vertices() = {a} by A1, GLIB_001:90; :: thesis: verum