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:77;
hence (T .pathBetween a,b) .vertices() c= the_Vertices_of t ; :: thesis: verum