let T be _Tree; :: thesis: for a, b being Vertex of T

for t being _Subtree of T st a in the_Vertices_of t & b in the_Vertices_of t holds

(T .pathBetween (a,b)) .vertices() c= the_Vertices_of t

let a, b be Vertex of T; :: thesis: for t being _Subtree of T st a in the_Vertices_of t & b in the_Vertices_of t holds

(T .pathBetween (a,b)) .vertices() c= the_Vertices_of t

let t be _Subtree of T; :: thesis: ( a in the_Vertices_of t & b in the_Vertices_of t implies (T .pathBetween (a,b)) .vertices() c= the_Vertices_of t )

assume ( a in the_Vertices_of t & b in the_Vertices_of t ) ; :: thesis: (T .pathBetween (a,b)) .vertices() c= the_Vertices_of t

then reconsider a9 = a, b9 = b as Vertex of t ;

set Tp = T .pathBetween (a,b);

set tp = t .pathBetween (a9,b9);

(T .pathBetween (a,b)) .vertices() = (t .pathBetween (a9,b9)) .vertices() by Th33, GLIB_001:76;

hence (T .pathBetween (a,b)) .vertices() c= the_Vertices_of t ; :: thesis: verum

for t being _Subtree of T st a in the_Vertices_of t & b in the_Vertices_of t holds

(T .pathBetween (a,b)) .vertices() c= the_Vertices_of t

let a, b be Vertex of T; :: thesis: for t being _Subtree of T st a in the_Vertices_of t & b in the_Vertices_of t holds

(T .pathBetween (a,b)) .vertices() c= the_Vertices_of t

let t be _Subtree of T; :: thesis: ( a in the_Vertices_of t & b in the_Vertices_of t implies (T .pathBetween (a,b)) .vertices() c= the_Vertices_of t )

assume ( a in the_Vertices_of t & b in the_Vertices_of t ) ; :: thesis: (T .pathBetween (a,b)) .vertices() c= the_Vertices_of t

then reconsider a9 = a, b9 = b as Vertex of t ;

set Tp = T .pathBetween (a,b);

set tp = t .pathBetween (a9,b9);

(T .pathBetween (a,b)) .vertices() = (t .pathBetween (a9,b9)) .vertices() by Th33, GLIB_001:76;

hence (T .pathBetween (a,b)) .vertices() c= the_Vertices_of t ; :: thesis: verum