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 S1[ 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 S1[k] holds
k <= 2 * (() + 1)
let k be Nat; :: thesis: ( S1[k] implies k <= 2 * (() + 1) )
assume S1[k] ; :: thesis: k <= 2 * (() + 1)
then consider P being Path of G such that
A3: len P = k ;
2 * (len ()) <= 2 * (() + 1) by ;
then k + 1 <= 2 * (() + 1) by ;
then (k + 1) - 1 <= (2 * (() + 1)) - 0 by XREAL_1:13;
hence k <= 2 * (() + 1) ; :: thesis: verum
end;
set src = () . the Element of the_Edges_of G;
set tar = () . the Element of the_Edges_of G;
the Element of the_Edges_of G Joins () . the Element of the_Edges_of G,() . the Element of the_Edges_of G,G by ;
then A4: len (G .walkOf ((() . the Element of the_Edges_of G), the Element of the_Edges_of G,(() . the Element of the_Edges_of G))) = 3 by GLIB_001:14;
then A5: ex k being Nat st S1[k] ;
consider k being Nat such that
A6: ( S1[k] & ( for n being Nat st S1[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 S1[n] holds
n <= k by A6;
A9: len () = k by ;
A10: 3 <= len W by A4, A7, A8;
then A11: not W is trivial by GLIB_001:125;
A12: now :: thesis: not W .first() = W .last() 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:
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: not W is trivial by ;
now :: thesis:
W .last() in W .vertices() by GLIB_001:88;
then not W .last() is isolated by ;
then (W .last()) .degree() <> 0 by GLIB_000:def 50;
then card () <> 0 by GLIB_000:19;
then 0 < card () by NAT_1:3;
then A19: 0 + 1 <= card () by NAT_1:13;
assume not W .last() is endvertex ; :: thesis: contradiction
then (W .last()) .degree() <> 1 by GLIB_000:def 52;
then card () <> 1 by GLIB_000:19;
then 1 < card () by ;
then consider e1, e2 being set such that
A20: e1 in () .edgesInOut() and
A21: ( e2 in () .edgesInOut() & e1 <> e2 ) by NAT_1:59;
now :: thesis: ex e2 being set st
( e2 in () .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 () .edgesInOut() & e2 <> W . (lenW2 + 1) )

take e2 = e2; :: thesis: ( e2 in () .edgesInOut() & e2 <> W . (lenW2 + 1) )
thus ( e2 in () .edgesInOut() & e2 <> W . (lenW2 + 1) ) by ; :: thesis: verum
end;
suppose A23: e1 <> W . (lenW2 + 1) ; :: thesis: ex e1 being set st
( e1 in () .edgesInOut() & e1 <> W . (lenW2 + 1) )

take e1 = e1; :: thesis: ( e1 in () .edgesInOut() & e1 <> W . (lenW2 + 1) )
thus ( e1 in () .edgesInOut() & e1 <> W . (lenW2 + 1) ) by ; :: thesis: verum
end;
end;
end;
then consider e being set such that
A24: e in () .edgesInOut() and
A25: e <> W . (lenW2 + 1) ;
consider v being Vertex of G such that
A26: e Joins W .last() ,v,G by ;
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 ;
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 ;
W . (W .rfind n) = v by ;
then A31: (W .cut ((W .rfind n),(len W))) .first() = v by ;
A32: e in ((W .cut ((W .rfind n),(len W))) .last()) .edgesInOut() by ;
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: not (W .cut ((W .rfind n),(len W))) .addEdge e is trivial by ;
( ((W .cut ((W .rfind n),(len W))) .addEdge e) .first() = v & ((W .cut ((W .rfind n),(len W))) .addEdge e) .last() = v ) by ;
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 ;
then (W .cut ((W .rfind n),(len W))) .addEdge e is Cycle-like by ;
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 ;
reconsider a1 = a - 1 as odd Element of NAT by ;
A40: a1 < (len W) - 0 by ;
a < lenW2 + 2 by ;
then a + 1 <= (lenW2 + 1) + 1 by NAT_1:13;
then a <= lenW2 + 1 by XREAL_1:6;
then A41: a < lenW2 + 1 by ;
a1 + 1 = a ;
then A42: e Joins W . a1,W . (a1 + 2),G by ;
per cases ( ( W .last() = W . a1 & v = W . (a1 + 2) ) or ( W .last() = W . (a1 + 2) & v = W . a1 ) ) by ;
suppose ( W .last() = W . a1 & v = W . (a1 + 2) ) ; :: thesis: contradiction
end;
suppose A43: ( W .last() = W . (a1 + 2) & v = W . a1 ) ; :: thesis: contradiction
a1 < (lenW2 + 1) - 1 by ;
then A44: a1 + 2 < len W by ;
W . (len W) = W . (a1 + 2) by ;
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;
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 () by Def5;
W .reverse() is open by ;
then (W .reverse()) .last() is endvertex by ;
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 ; :: thesis: verum