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;

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

( 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

1 <= len W
by ABIAN:12;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;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

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