let G2 be _Graph; :: thesis: for v, e, x being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W2 is minlength & W2 is_Walk_from x,w & not e in the_Edges_of G2 holds
W1 .addEdge e is minlength
let v, e, x be object ; :: thesis: for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W2 is minlength & W2 is_Walk_from x,w & not e in the_Edges_of G2 holds
W1 .addEdge e is minlength
let w be Vertex of G2; :: thesis: for G1 being addAdjVertex of G2,v,e,w
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W2 is minlength & W2 is_Walk_from x,w & not e in the_Edges_of G2 holds
W1 .addEdge e is minlength
let G1 be addAdjVertex of G2,v,e,w; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W2 is minlength & W2 is_Walk_from x,w & not e in the_Edges_of G2 holds
W1 .addEdge e is minlength
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 & W2 is minlength & W2 is_Walk_from x,w & not e in the_Edges_of G2 holds
W1 .addEdge e is minlength
let W2 be Walk of G2; :: thesis: ( W1 = W2 & W2 is minlength & W2 is_Walk_from x,w & not e in the_Edges_of G2 implies W1 .addEdge e is minlength )
assume that
A1: ( W1 = W2 & W2 is minlength & W2 is_Walk_from x,w ) and
A2: not e in the_Edges_of G2 ; :: thesis: W1 .addEdge e is minlength

per cases ( not v in the_Vertices_of G2 or v in the_Vertices_of G2 ) ;

suppose A3: not v in the_Vertices_of G2 ; :: thesis: W1 .addEdge e is minlength

then e Joins v,w,G1 by A2, GLIB_006:132;
then A4: e Joins w,v,G1 by GLIB_000:14;
A5: w = W2 .last() by A1, GLIB_001:def 23
.= W1 .last() by A1 ;

now :: thesis: for W3 being Walk of G1 st W3 is_Walk_from (W1 .addEdge e) .first() ,(W1 .addEdge e) .last() holds
len W3 >= len (W1 .addEdge e)

let W3 be Walk of G1; :: thesis: ( W3 is_Walk_from (W1 .addEdge e) .first() ,(W1 .addEdge e) .last() implies len W3 >= len (W1 .addEdge e) )
assume W3 is_Walk_from (W1 .addEdge e) .first() ,(W1 .addEdge e) .last() ; :: thesis: len W3 >= len (W1 .addEdge e)
then W3 is_Walk_from W1 .first() ,(W1 .addEdge e) .last() by A4, A5, GLIB_001:63;
then A6: W3 is_Walk_from W1 .first() ,v by A4, A5, GLIB_001:63;
then A7: W3 is_Walk_from W2 .first() ,v by A1;

now :: thesis: W3 is trivial

assume A8: W3 is trivial ; :: thesis: contradiction
W2 .first() = W3 .first() by A7, GLIB_001:def 23
.= W3 .last() by A8, GLIB_001:127
.= v by A7, GLIB_001:def 23 ;
hence contradiction by A3; :: thesis: verum

end;

then A9: 3 - 2 <= (len W3) - 2 by GLIB_001:125, XREAL_1:9;
then reconsider m = (len W3) - 2 as odd Element of NAT by INT_1:3, POLYFORM:5;
A10: ( m < (len W3) - 0 & m <= (len W3) - 0 ) by XREAL_1:10;
then W3 . (m + 1) Joins W3 . m,W3 . (m + 2),G1 by GLIB_001:def 3;
then W3 . (m + 1) Joins W3 . m,W3 .last() ,G1 ;
then W3 . (m + 1) Joins W3 . m,v,G1 by A7, GLIB_001:def 23;
then W3 . (m + 1) Joins v,W3 . m,G1 by GLIB_000:14;
then A11: W3 . m = w by A2, A3, GLIB_006:134;
set W = W3 .cut (1,m);
W3 .cut (1,m) is_Walk_from W3 . 1,W3 . m by A9, A10, GLIB_001:37, POLYFORM:4;
then W3 .cut (1,m) is_Walk_from W3 .first() ,W3 . m ;
then W3 .cut (1,m) is_Walk_from W1 .first() ,W3 . m by A6, GLIB_001:def 23;
then W3 .cut (1,m) is_Walk_from W1 .first() ,W2 .last() by A1, A11, GLIB_001:def 23;
then A12: W3 .cut (1,m) is_Walk_from W1 .first() ,W1 .last() by A1;
A13: (len (W3 .cut (1,m))) + 1 = m + 1 by A9, A10, GLIB_001:36, POLYFORM:4;
W1 is minlength by A1, Th61;
then (len (W3 .cut (1,m))) + 2 >= (len W1) + 2 by A12, CHORD:def 2, XREAL_1:6;
hence len W3 >= len (W1 .addEdge e) by A4, A5, A13, GLIB_001:64; :: thesis: verum

end;

hence W1 .addEdge e is minlength by CHORD:def 2; :: thesis: verum

end;

suppose v in the_Vertices_of G2 ; :: thesis: W1 .addEdge e is minlength

then G1 == G2 by GLIB_006:def 12;
then not e in the_Edges_of G1 by A2, GLIB_000:def 34;
then not e in (W1 .last()) .edgesInOut() ;
hence W1 .addEdge e is minlength by A1, Th36, Th61; :: thesis: verum

end;

end;