let G2 be _Graph; :: thesis: for v, e, w being object
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 holds
W1 is minlength
let v, e, w be object ; :: 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 holds
W1 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 holds
W1 is minlength
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 & W2 is minlength holds
W1 is minlength
let W2 be Walk of G2; :: thesis: ( W1 = W2 & W2 is minlength implies W1 is minlength )
assume A1: ( W1 = W2 & W2 is minlength ) ; :: thesis: W1 is minlength
then ( W1 .first() = W2 .first() & W1 .last() = W2 .last() ) ;
then A2: ( W1 .first() in the_Vertices_of G2 & W1 .last() in the_Vertices_of G2 ) ;

per cases ( ( not e in the_Edges_of G2 & not v in the_Vertices_of G2 & w in the_Vertices_of G2 ) or ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 & v in the_Vertices_of G2 ) or ( not ( not e in the_Edges_of G2 & not v in the_Vertices_of G2 & w in the_Vertices_of G2 ) & not ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 & v in the_Vertices_of G2 ) ) ) ;

suppose A3: ( not e in the_Edges_of G2 & not v in the_Vertices_of G2 & w in the_Vertices_of G2 ) ; :: thesis: W1 is minlength

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

let W3 be Walk of G1; :: thesis: ( W3 is_Walk_from W1 .first() ,W1 .last() implies len W3 >= len W1 )
assume A4: W3 is_Walk_from W1 .first() ,W1 .last() ; :: thesis: len W3 >= len W1
set T = the Trail of W3;
A5: the Trail of W3 is_Walk_from W1 .first() ,W1 .last() by A4, GLIB_001:160;
then A6: ( the Trail of W3 .first() = W1 .first() & the Trail of W3 .last() = W1 .last() ) by GLIB_001:def 23;
then A7: not e in the Trail of W3 .edges() by A2, A3, GLIB_006:147;
the Trail of W3 is Walk of G2

proof

per cases ( not the Trail of W3 is trivial or not the Trail of W3 is trivial ) ;

suppose the Trail of W3 is trivial ; :: thesis: the Trail of W3 is Walk of G2

then consider v0 being Vertex of G1 such that
A8: the Trail of W3 = G1 .walkOf v0 by GLIB_001:128;
A9: v0 in the_Vertices_of G2 by A2, A6, A8;
the Trail of W3 .vertices() = {v0} by A8, GLIB_001:90;
then not v in the Trail of W3 .vertices() by A3, A9, TARSKI:def 1;
hence the Trail of W3 is Walk of G2 by A3, GLIB_006:146; :: thesis: verum

end;

suppose the Trail of W3 is trivial ; :: thesis: the Trail of W3 is Walk of G2

hence the Trail of W3 is Walk of G2 by A3, A7, GLIB_006:146; :: thesis: verum

end;

end;

end;

then reconsider W4 = the Trail of W3 as Walk of G2 ;
W4 is_Walk_from W1 .first() ,W1 .last() by A5, GLIB_001:19;
then W4 is_Walk_from W2 .first() ,W1 .last() by A1;
then W4 is_Walk_from W2 .first() ,W2 .last() by A1;
then A10: len the Trail of W3 >= len W1 by A1, CHORD:def 2;
len W3 >= len the Trail of W3 by GLIB_001:162;
hence len W3 >= len W1 by A10, XXREAL_0:2; :: thesis: verum

end;

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

end;

suppose A11: ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 & v in the_Vertices_of G2 ) ; :: thesis: W1 is minlength

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

let W3 be Walk of G1; :: thesis: ( W3 is_Walk_from W1 .first() ,W1 .last() implies len W3 >= len W1 )
assume A12: W3 is_Walk_from W1 .first() ,W1 .last() ; :: thesis: len W3 >= len W1
set T = the Trail of W3;
A13: the Trail of W3 is_Walk_from W1 .first() ,W1 .last() by A12, GLIB_001:160;
then A14: ( the Trail of W3 .first() = W1 .first() & the Trail of W3 .last() = W1 .last() ) by GLIB_001:def 23;
then A15: not e in the Trail of W3 .edges() by A2, A11, GLIB_006:147;
the Trail of W3 is Walk of G2

proof

per cases ( not the Trail of W3 is trivial or not the Trail of W3 is trivial ) ;

suppose the Trail of W3 is trivial ; :: thesis: the Trail of W3 is Walk of G2

then consider v0 being Vertex of G1 such that
A16: the Trail of W3 = G1 .walkOf v0 by GLIB_001:128;
A17: v0 in the_Vertices_of G2 by A2, A14, A16;
the Trail of W3 .vertices() = {v0} by A16, GLIB_001:90;
then not w in the Trail of W3 .vertices() by A11, A17, TARSKI:def 1;
hence the Trail of W3 is Walk of G2 by A11, GLIB_006:145; :: thesis: verum

end;

suppose the Trail of W3 is trivial ; :: thesis: the Trail of W3 is Walk of G2

hence the Trail of W3 is Walk of G2 by A11, A15, GLIB_006:145; :: thesis: verum

end;

end;

end;

then reconsider W4 = the Trail of W3 as Walk of G2 ;
W4 is_Walk_from W1 .first() ,W1 .last() by A13, GLIB_001:19;
then W4 is_Walk_from W2 .first() ,W1 .last() by A1;
then W4 is_Walk_from W2 .first() ,W2 .last() by A1;
then A18: len the Trail of W3 >= len W1 by A1, CHORD:def 2;
len W3 >= len the Trail of W3 by GLIB_001:162;
hence len W3 >= len W1 by A18, XXREAL_0:2; :: thesis: verum

end;

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

end;

suppose ( not ( not e in the_Edges_of G2 & not v in the_Vertices_of G2 & w in the_Vertices_of G2 ) & not ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 & v in the_Vertices_of G2 ) ) ; :: thesis: W1 is minlength

then G1 == G2 by GLIB_006:def 12;
hence W1 is minlength by A1, Th49; :: thesis: verum

end;

end;