let G be finite non trivial acyclic _Graph; :: thesis: ( the_Edges_of G <> {} implies ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G .reachableFrom v1 ) )
assume A1: the_Edges_of G <> {} ; :: thesis: ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G .reachableFrom v1 )
set e = choose (the_Edges_of G);
defpred S₁[ Nat] means ex W being Path of G st len W = $1;

A2: now

let k be Nat; :: thesis: ( S₁[k] implies k <= 2 * ((G .order() ) + 1) )
assume S₁[k] ; :: thesis: k <= 2 * ((G .order() ) + 1)
then consider P being Path of G such that
A3: len P = k ;
2 * (len (P .vertexSeq() )) <= 2 * ((G .order() ) + 1) by GLIB_001:155, XREAL_1:66;
then k + 1 <= 2 * ((G .order() ) + 1) by A3, GLIB_001:def 14;
then (k + 1) - 1 <= (2 * ((G .order() ) + 1)) - 0 by XREAL_1:15;
hence k <= 2 * ((G .order() ) + 1) ; :: thesis: verum

end;

set src = (the_Source_of G) . (choose (the_Edges_of G));
set tar = (the_Target_of G) . (choose (the_Edges_of G));
choose (the_Edges_of G) Joins (the_Source_of G) . (choose (the_Edges_of G)),(the_Target_of G) . (choose (the_Edges_of G)),G by A1, GLIB_000:def 15;
then A4: len (G .walkOf ((the_Source_of G) . (choose (the_Edges_of G))),(choose (the_Edges_of G)),((the_Target_of G) . (choose (the_Edges_of G)))) = 3 by GLIB_001:15;
then A5: ex k being Nat st S₁[k] ;
consider k being Nat such that
A6: ( S₁[k] & ( for n being Nat st S₁[n] holds
n <= k ) ) from NAT_1:sch 6(A2, A5);
consider W being Path of G such that
A7: ( len W = k & ( for n being Nat st S₁[n] holds
n <= k ) ) by A6;
A8: 3 <= len W by A4, A7;
then A9: not W is trivial by GLIB_001:126;

A10: now

assume W .first() = W .last() ; :: thesis: contradiction
then W is closed by GLIB_001:def 24;
then W is Cycle-like by A9, GLIB_001:def 31;
hence contradiction by Def2; :: thesis: verum

end;

then A11: not W is closed by GLIB_001:def 24;

A12: now

let W be Path of G; :: thesis: ( len W = k & not W is closed implies W .last() is endvertex )
assume A13: ( len W = k & not W is closed ) ; :: thesis: W .last() is endvertex
then A14: not W is trivial by A7, A8, GLIB_001:126;
2 + 1 <= len W by A4, A7, A13;
then 2 < len W by NAT_1:13;
then reconsider lenW2 = (len W) - (2 * 1) as odd Element of NAT by INT_1:18;
A15: lenW2 + 2 = len W ;

now

assume not W .last() is endvertex ; :: thesis: contradiction
then (W .last() ) .degree() <> 1 by GLIB_000:def 54;
then A16: card ((W .last() ) .edgesInOut() ) <> 1 by GLIB_000:22;
W .last() in W .vertices() by GLIB_001:89;
then not W .last() is isolated by A14, GLIB_001:136;
then (W .last() ) .degree() <> 0 by GLIB_000:def 52;
then card ((W .last() ) .edgesInOut() ) <> 0 by GLIB_000:22;
then 0 < card ((W .last() ) .edgesInOut() ) by NAT_1:3;
then 0 + 1 <= card ((W .last() ) .edgesInOut() ) by NAT_1:13;
then 1 < card ((W .last() ) .edgesInOut() ) by A16, XXREAL_0:1;
then consider e1, e2 being set such that
A17: ( e1 in (W .last() ) .edgesInOut() & e2 in (W .last() ) .edgesInOut() & e1 <> e2 ) by Th1;

now

per cases ( e1 = W . (lenW2 + 1) or e1 <> W . (lenW2 + 1) ) ;

suppose A18: e1 = W . (lenW2 + 1) ; :: thesis: ex e2 being set st
( e2 in (W .last() ) .edgesInOut() & e2 <> W . (lenW2 + 1) )

take e2 = e2; :: thesis: ( e2 in (W .last() ) .edgesInOut() & e2 <> W . (lenW2 + 1) )
thus ( e2 in (W .last() ) .edgesInOut() & e2 <> W . (lenW2 + 1) ) by A17, A18; :: thesis: verum

end;

suppose A19: e1 <> W . (lenW2 + 1) ; :: thesis: ex e1 being set st
( e1 in (W .last() ) .edgesInOut() & e1 <> W . (lenW2 + 1) )

take e1 = e1; :: thesis: ( e1 in (W .last() ) .edgesInOut() & e1 <> W . (lenW2 + 1) )
thus ( e1 in (W .last() ) .edgesInOut() & e1 <> W . (lenW2 + 1) ) by A17, A19; :: thesis: verum

end;

end;

end;

then consider e being set such that
A20: ( e in (W .last() ) .edgesInOut() & e <> W . (lenW2 + 1) ) ;
consider v being Vertex of G such that
A21: e Joins W .last() ,v,G by A20, GLIB_000:67;

now

per cases ( v in W .vertices() or not v in W .vertices() ) ;

suppose v in W .vertices() ; :: thesis: contradiction

then consider n being odd Element of NAT such that
A22: ( n <= len W & W . n = v ) by GLIB_001:88;
set m = W .rfind n;
A23: ( W .rfind n <= len W & W . (W .rfind n) = v & ( for k being odd Element of NAT st k <= len W & W . k = v holds
k <= W .rfind n ) ) by A22, GLIB_001:def 22;
set W2 = W .cut (W .rfind n),(len W);
A24: ( (W .cut (W .rfind n),(len W)) .first() = v & (W .cut (W .rfind n),(len W)) .last() = W . (len W) ) by A23, GLIB_001:38;
then A25: e Joins (W .cut (W .rfind n),(len W)) .last() ,v,G by A21, GLIB_001:def 7;
then A26: e in ((W .cut (W .rfind n),(len W)) .last() ) .edgesInOut() by GLIB_000:65;

now

per cases ( not e in (W .cut (W .rfind n),(len W)) .edges() or e in (W .cut (W .rfind n),(len W)) .edges() ) ;

suppose not e in (W .cut (W .rfind n),(len W)) .edges() ; :: thesis: contradiction

then A27: (W .cut (W .rfind n),(len W)) .addEdge e is Path-like by A26, Lm22;
( ((W .cut (W .rfind n),(len W)) .addEdge e) .first() = v & ((W .cut (W .rfind n),(len W)) .addEdge e) .last() = v ) by A24, A25, GLIB_001:64;
then A28: (W .cut (W .rfind n),(len W)) .addEdge e is closed by GLIB_001:def 24;
not (W .cut (W .rfind n),(len W)) .addEdge e is trivial by A25, GLIB_001:133;
then (W .cut (W .rfind n),(len W)) .addEdge e is Cycle-like by A27, A28, GLIB_001:def 31;
hence contradiction by Def2; :: thesis: verum

end;

suppose A29: e in (W .cut (W .rfind n),(len W)) .edges() ; :: thesis: contradiction

(W .cut (W .rfind n),(len W)) .edges() c= W .edges() by GLIB_001:107;
then consider a being even Element of NAT such that
A30: ( 1 <= a & a <= len W & W . a = e ) by A29, GLIB_001:100;
a < lenW2 + 2 by A30, XXREAL_0:1;
then a + 1 <= (lenW2 + 1) + 1 by NAT_1:13;
then a <= lenW2 + 1 by XREAL_1:8;
then A31: a < lenW2 + 1 by A20, A30, XXREAL_0:1;
reconsider a1 = a - 1 as odd Element of NAT by A30, INT_1:18;
A32: a1 < (len W) - 0 by A30, XREAL_1:17;
a1 + 1 = a ;
then A33: e Joins W . a1,W . (a1 + 2),G by A30, A32, GLIB_001:def 3;

now

per cases ( ( W .last() = W . a1 & v = W . (a1 + 2) ) or ( W .last() = W . (a1 + 2) & v = W . a1 ) ) by A21, A33, GLIB_000:18;

suppose ( W .last() = W . a1 & v = W . (a1 + 2) ) ; :: thesis: contradiction

then W . (len W) = W . a1 by GLIB_001:def 7;
hence contradiction by A13, A32, GLIB_001:148; :: thesis: verum

end;

suppose ( W .last() = W . (a1 + 2) & v = W . a1 ) ; :: thesis: contradiction

then A34: W . (len W) = W . (a1 + 2) by GLIB_001:def 7;
a1 < (lenW2 + 1) - 1 by A31, XREAL_1:16;
then a1 + 2 < len W by A15, XREAL_1:10;
hence contradiction by A13, A34, GLIB_001:148; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose not v in W .vertices() ; :: thesis: contradiction

then A35: W .addEdge e is Path-like by A13, A21, GLIB_001:152;
len (W .addEdge e) = k + 2 by A13, A21, GLIB_001:65;
then k + 2 <= k + 0 by A7, A35;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence W .last() is endvertex ; :: thesis: verum

end;

then A36: W .last() is endvertex by A7, A11;
A37: len (W .reverse() ) = k by A7, GLIB_001:22;
not W .reverse() is closed by A11, GLIB_001:121;
then (W .reverse() ) .last() is endvertex by A12, A37;
then A38: W .first() is endvertex by GLIB_001:23;
W is_Walk_from W .first() ,W .last() by GLIB_001:def 23;
then W .last() in G .reachableFrom (W .first() ) by Def5;
hence ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G .reachableFrom v1 ) by A10, A36, A38; :: thesis: verum