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_{1}[ Nat] means ex W being Path of G st len W = $1;

set e = 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_{1}[k]
;

consider k being Nat such that

A6: ( S_{1}[k] & ( for n being Nat st S_{1}[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_{1}[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: not W is trivial by GLIB_001:125;

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

( 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

set e = the Element of the_Edges_of G;

A2: now :: thesis: for k being Nat st S_{1}[k] holds

k <= 2 * ((G .order()) + 1)

set src = (the_Source_of G) . the Element of the_Edges_of G;k <= 2 * ((G .order()) + 1)

let k be Nat; :: thesis: ( S_{1}[k] implies k <= 2 * ((G .order()) + 1) )

assume S_{1}[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;assume S

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

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

consider k being Nat such that

A6: ( S

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 <= k by A6;

A9: len (W .reverse()) = k by A7, GLIB_001:21;

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()

then A13:
W is open
by GLIB_001:def 24;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 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

A14: now :: thesis: for W being Path of G st len W = k & W is open holds

W .last() is endvertex

W is_Walk_from W .first() ,W .last()
by GLIB_001:def 23;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: not W is trivial by A7, A10, A15, GLIB_001:125;

end;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: not W is trivial by A7, A10, A15, GLIB_001:125;

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

hence
W .last() is endvertex
; :: thesis: verum
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;

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;

end;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) )end;

then consider e being set such that ( e2 in (W .last()) .edgesInOut() & e2 <> W . (lenW2 + 1) )

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

end;

suppose A22:
e1 = W . (lenW2 + 1)
; :: thesis: ex e2 being set st

( e2 in (W .last()) .edgesInOut() & e2 <> W . (lenW2 + 1) )

( 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;thus ( e2 in (W .last()) .edgesInOut() & e2 <> W . (lenW2 + 1) ) by A21, A22; :: thesis: verum

suppose A23:
e1 <> W . (lenW2 + 1)
; :: thesis: ex e1 being set st

( e1 in (W .last()) .edgesInOut() & e1 <> W . (lenW2 + 1) )

( 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;thus ( e1 in (W .last()) .edgesInOut() & e1 <> W . (lenW2 + 1) ) by A20, A23; :: thesis: verum

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: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( v in W .vertices() or not v in W .vertices() )
;

end;

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;

end;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: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( not e in (W .cut ((W .rfind n),(len W))) .edges() or e in (W .cut ((W .rfind n),(len W))) .edges() )
;

end;

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 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;( ((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

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;

end;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: contradictionend;

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

end;

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

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;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

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;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

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