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 that
A1: a in the_Vertices_of t and
A2: b in the_Vertices_of t ; :: thesis: (T .pathBetween a,b) .vertices() c= the_Vertices_of t
reconsider a' = a, b' = b as Vertex of t by A1, A2;
set Tp = T .pathBetween a,b;
set tp = t .pathBetween a',b';
(T .pathBetween a,b) .vertices() = (t .pathBetween a',b') .vertices() by Th32, GLIB_001:77;
hence (T .pathBetween a,b) .vertices() c= the_Vertices_of t ; :: thesis: verum