theorem Th31: :: GLIB_008:31

for G1 being _finite non _trivial Tree-like _Graph
for G2 being non spanning connected Subgraph of G1 ex v being Vertex of G1 st
( v is endvertex & not v in the_Vertices_of G2 )