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 )
defpred S₁[ Nat] means ex W being Path of G st len W = $1;
set e = the Element of the_Edges_of G;

A2: now :: thesis: for k being Nat st S₁[k] holds
k <= 2 * ((G .order()) + 1)

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:154, XREAL_1:64;
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:13;
hence k <= 2 * ((G .order()) + 1) ; :: thesis: verum

end;

set src = (the_Source_of G) . the Element of the_Edges_of G;
set tar = (the_Target_of G) . the Element of the_Edges_of G;
the Element of the_Edges_of G Joins (the_Source_of G) . the Element of the_Edges_of G,(the_Target_of G) . the Element of the_Edges_of G,G by A1, GLIB_000:def 13;
then A4: len (G .walkOf (((the_Source_of G) . the Element of the_Edges_of G), the Element of the_Edges_of G,((the_Target_of G) . the Element of the_Edges_of G))) = 3 by GLIB_001:14;
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 and
A8: for n being Nat st S₁[n] holds
n <= k by A6;
A9: len (W .reverse()) = k by A7, GLIB_001:21;
A10: 3 <= len W by A4, A7, A8;
then A11: W is trivial by GLIB_001:125;

A12: now :: thesis: not W .first() = W .last()

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

end;

then A13: W is open by GLIB_001:def 24;

A14: now :: thesis: for W being Path of G st len W = k & W is open holds
W .last() is endvertex

let W be Path of G; :: thesis: ( len W = k & W is open implies W .last() is endvertex )
assume that
A15: len W = k and
A16: W is open ; :: thesis: W .last() is endvertex
2 + 1 <= len W by A4, A8, A15;
then 2 < len W by NAT_1:13;
then reconsider lenW2 = (len W) - (2 * 1) as odd Element of NAT by INT_1:5;
A17: lenW2 + 2 = len W ;
A18: W is trivial by A7, A10, A15, GLIB_001:125;

now :: thesis: W .last() is endvertex

W .last() in W .vertices() by GLIB_001:88;
then not W .last() is isolated by A18, GLIB_001:135;
then (W .last()) .degree() <> 0 by GLIB_000:def 50;
then card ((W .last()) .edgesInOut()) <> 0 by GLIB_000:19;
then 0 < card ((W .last()) .edgesInOut()) by NAT_1:3;
then A19: 0 + 1 <= card ((W .last()) .edgesInOut()) by NAT_1:13;
assume not W .last() is endvertex ; :: thesis: contradiction
then (W .last()) .degree() <> 1 by GLIB_000:def 52;
then card ((W .last()) .edgesInOut()) <> 1 by GLIB_000:19;
then 1 < card ((W .last()) .edgesInOut()) by A19, XXREAL_0:1;
then consider e1, e2 being set such that
A20: e1 in (W .last()) .edgesInOut() and
A21: ( e2 in (W .last()) .edgesInOut() & e1 <> e2 ) by NAT_1:59;

now :: thesis: ex e2 being set st
( e2 in (W .last()) .edgesInOut() & e2 <> W . (lenW2 + 1) )

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

suppose A22: 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 A21, A22; :: thesis: verum

end;

suppose A23: 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 A20, A23; :: thesis: verum

end;

end;

end;

then consider e being set such that
A24: e in (W .last()) .edgesInOut() and
A25: e <> W . (lenW2 + 1) ;
consider v being Vertex of G such that
A26: e Joins W .last() ,v,G by A24, GLIB_000:64;

now :: thesis: contradiction

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
A27: n <= len W and
A28: W . n = v by GLIB_001:87;
set m = W .rfind n;
set W2 = W .cut ((W .rfind n),(len W));
A29: W .rfind n <= len W by A27, GLIB_001:def 22;
then (W .cut ((W .rfind n),(len W))) .last() = W . (len W) by GLIB_001:37;
then A30: e Joins (W .cut ((W .rfind n),(len W))) .last() ,v,G by A26, GLIB_001:def 7;
W . (W .rfind n) = v by A27, A28, GLIB_001:def 22;
then A31: (W .cut ((W .rfind n),(len W))) .first() = v by A29, GLIB_001:37;
A32: e in ((W .cut ((W .rfind n),(len W))) .last()) .edgesInOut() by A30, GLIB_000:62;

now :: thesis: contradiction

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 A33: not e in (W .cut ((W .rfind n),(len W))) .edges() ; :: thesis: contradiction

A34: (W .cut ((W .rfind n),(len W))) .addEdge e is trivial by A30, GLIB_001:132;
( ((W .cut ((W .rfind n),(len W))) .addEdge e) .first() = v & ((W .cut ((W .rfind n),(len W))) .addEdge e) .last() = v ) by A31, A30, GLIB_001:63;
then A35: (W .cut ((W .rfind n),(len W))) .addEdge e is closed by GLIB_001:def 24;
(W .cut ((W .rfind n),(len W))) .addEdge e is Path-like by A32, A33, Lm22;
then (W .cut ((W .rfind n),(len W))) .addEdge e is Cycle-like by A35, A34, GLIB_001:def 31;
hence contradiction by Def2; :: thesis: verum

end;

suppose A36: 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:106;
then consider a being even Element of NAT such that
A37: 1 <= a and
A38: a <= len W and
A39: W . a = e by A36, GLIB_001:99;
reconsider a1 = a - 1 as odd Element of NAT by A37, INT_1:5;
A40: a1 < (len W) - 0 by A38, XREAL_1:15;
a < lenW2 + 2 by A38, XXREAL_0:1;
then a + 1 <= (lenW2 + 1) + 1 by NAT_1:13;
then a <= lenW2 + 1 by XREAL_1:6;
then A41: a < lenW2 + 1 by A25, A39, XXREAL_0:1;
a1 + 1 = a ;
then A42: e Joins W . a1,W . (a1 + 2),G by A39, A40, GLIB_001:def 3;

now :: thesis: contradiction

per cases ( ( W .last() = W . a1 & v = W . (a1 + 2) ) or ( W .last() = W . (a1 + 2) & v = W . a1 ) ) by A26, A42, GLIB_000:15;

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 A16, A40, GLIB_001:147; :: thesis: verum

end;

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

a1 < (lenW2 + 1) - 1 by A41, XREAL_1:14;
then A44: a1 + 2 < len W by A17, XREAL_1:8;
W . (len W) = W . (a1 + 2) by A43, GLIB_001:def 7;
hence contradiction by A16, A44, GLIB_001:147; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

A46: len (W .addEdge e) = k + 2 by A15, A26, GLIB_001:64;
W .addEdge e is Path-like by A16, A26, A45, GLIB_001:151;
then k + 2 <= k + 0 by A8, A46;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

end;

W is_Walk_from W .first() ,W .last() by GLIB_001:def 23;
then A47: W .last() in G .reachableFrom (W .first()) by Def5;
W .reverse() is open by A13, GLIB_001:120;
then (W .reverse()) .last() is endvertex by A14, A9;
then A48: W .first() is endvertex by GLIB_001:22;
W .last() is endvertex by A7, A13, A14;
hence ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G .reachableFrom v1 ) by A12, A48, A47; :: thesis: verum