theorem Th30: :: GLIB_008:30

for T being _finite non _trivial _Tree
for v being Vertex of T ex v1, v2 being Vertex of T st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v in (T .pathBetween (v1,v2)) .vertices() )