let G1 be _finite non _trivial Tree-like _Graph; :: thesis: 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 )
let G2 be non spanning connected Subgraph of G1; :: thesis: ex v being Vertex of G1 st
( v is endvertex & not v in the_Vertices_of G2 )
assume A1: for v being Vertex of G1 holds
( not v is endvertex or v in the_Vertices_of G2 ) ; :: thesis: contradiction
A2: not the_Vertices_of G1 c= the_Vertices_of G2 by GLIB_000:def 33, XBOOLE_0:def 10;
for x being object st x in the_Vertices_of G1 holds
x in the_Vertices_of G2
proof
let x be object ; :: thesis: ( x in the_Vertices_of G1 implies x in the_Vertices_of G2 )
assume x in the_Vertices_of G1 ; :: thesis: x in the_Vertices_of G2
then reconsider v = x as Vertex of G1 ;
consider v1, v2 being Vertex of G1 such that
A3: ( v1 <> v2 & v1 is endvertex & v2 is endvertex ) and
A4: v in (G1 .pathBetween (v1,v2)) .vertices() by Th30;
reconsider w1 = v1, w2 = v2 as Vertex of G2 by A1, A3;
v in (G2 .pathBetween (w1,w2)) .vertices() by A4, HELLY:33, GLIB_001:98;
hence x in the_Vertices_of G2 ; :: thesis: verum
end;
hence contradiction by A2, TARSKI:def 3; :: thesis: verum