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