theorem :: GLIB_002:45
for G being _finite non _trivial Tree-like _Graph ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex ) by Lm24;