let G be _finite non _trivial Tree-like _Graph; :: thesis: ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex )
consider v1, v2 being Vertex of G such that
A1: v1 <> v2 by GLIB_000:21;
consider W being Walk of G such that
A2: W is_Walk_from v1,v2 by Def1;
A3: now :: thesis: not len W = 1
assume len W = 1 ; :: thesis: contradiction
then A4: W .last() = W . 1 by GLIB_001:def 7
.= W .first() by GLIB_001:def 6 ;
W .first() = v1 by A2, GLIB_001:def 23;
hence contradiction by A1, A2, A4, GLIB_001:def 23; :: thesis: verum
end;
1 <= len W by ABIAN:12;
then 1 < len W by A3, XXREAL_0:1;
then 1 + 1 <= len W by NAT_1:13;
then 1 + 1 in dom W by FINSEQ_3:25;
then W . (2 * 1) in the_Edges_of G by GLIB_001:8;
then ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G .reachableFrom v1 ) by Lm23;
hence ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex ) ; :: thesis: verum