let G2 be _Graph; 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 ; 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; 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; for W2 being Walk of G2 st W1 = W2 & W2 is minlength holds
W1 is minlength
let W2 be Walk of G2; ( W1 = W2 & W2 is minlength implies W1 is minlength )
assume A1:
( W1 = W2 & W2 is minlength )
; W1 is minlength
then
( W1 .first() = W2 .first() & W1 .last() = W2 .last() )
by GLIB_001:16;
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 )
;
W1 is minlength now for W3 being Walk of G1 st W3 is_Walk_from W1 .first() ,W1 .last() holds
len W3 >= len W1let W3 be
Walk of
G1;
( W3 is_Walk_from W1 .first() ,W1 .last() implies len W3 >= len W1 )assume A4:
W3 is_Walk_from W1 .first() ,
W1 .last()
;
len W3 >= len W1set 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
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, GLIB_001:16;
then
W4 is_Walk_from W2 .first() ,
W2 .last()
by A1, GLIB_001:16;
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;
verum end; hence
W1 is
minlength
by CHORD:def 2;
verum suppose A11:
( not
e in the_Edges_of G2 & not
w in the_Vertices_of G2 &
v in the_Vertices_of G2 )
;
W1 is minlength now for W3 being Walk of G1 st W3 is_Walk_from W1 .first() ,W1 .last() holds
len W3 >= len W1let W3 be
Walk of
G1;
( W3 is_Walk_from W1 .first() ,W1 .last() implies len W3 >= len W1 )assume A12:
W3 is_Walk_from W1 .first() ,
W1 .last()
;
len W3 >= len W1set 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
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, GLIB_001:16;
then
W4 is_Walk_from W2 .first() ,
W2 .last()
by A1, GLIB_001:16;
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;
verum end; hence
W1 is
minlength
by CHORD:def 2;
verum