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:24;
consider W being Walk of G such that
A2: W is_Walk_from v1,v2 by Def1;
A3: 1 <= len W by HEYTING3:1;

now

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 & W .last() = v2 ) by A2, GLIB_001:def 23;
hence contradiction by A1, A4; :: thesis: verum

end;

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:27;
then W . (2 * 1) in the_Edges_of G by GLIB_001:9;
then consider v1, v2 being Vertex of G such that
A5: ( v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G .reachableFrom v1 ) by Lm23;
thus ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex ) by A5; :: thesis: verum