let T be _Tree; :: thesis: for a, b being Vertex of
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 ; :: 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 a' = a, b' = b as Vertex of ;
set Tp = T .pathBetween a,b;
set tp = t .pathBetween a',b';
(T .pathBetween a,b) .vertices() = (t .pathBetween a',b') .vertices() by Th33, GLIB_001:77;
hence (T .pathBetween a,b) .vertices() c= the_Vertices_of t ; :: thesis: verum