let G be _Graph; :: thesis: for S being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,S
for W being Walk of H st W is minlength holds
for m, n being natural odd number st m + 2 < n & n <= len W holds
for e being set holds not e Joins W . m,W . n,G
let S be non empty Subset of (the_Vertices_of G); :: thesis: for H being inducedSubgraph of G,S
for W being Walk of H st W is minlength holds
for m, n being natural odd number st m + 2 < n & n <= len W holds
for e being set holds not e Joins W . m,W . n,G
let GA be inducedSubgraph of G,S; :: thesis: for W being Walk of GA st W is minlength holds
for m, n being natural odd number st m + 2 < n & n <= len W holds
for e being set holds not e Joins W . m,W . n,G
let P be Walk of GA; :: thesis: ( P is minlength implies for m, n being natural odd number st m + 2 < n & n <= len P holds
for e being set holds not e Joins P . m,P . n,G )
assume A1: P is minlength ; :: thesis: for m, n being natural odd number st m + 2 < n & n <= len P holds
for e being set holds not e Joins P . m,P . n,G
A2: S = the_Vertices_of GA by GLIB_000:def 39;

now

let m, n be odd Nat; :: thesis: ( m + 2 < n & n <= len P implies for e being set holds not e Joins P . m,P . n,G )
assume A3: ( m + 2 < n & n <= len P ) ; :: thesis: for e being set holds not e Joins P . m,P . n,G
A4: ( m in NAT & n in NAT ) by ORDINAL1:def 13;
let e be set ; :: thesis: not e Joins P . m,P . n,G
assume A5: e Joins P . m,P . n,G ; :: thesis: contradiction
m + 0 <= m + 2 by XREAL_1:9;
then m <= n by A3, XXREAL_0:2;
then ( P . m in the_Vertices_of GA & P . n in the_Vertices_of GA ) by A3, A4, GLIB_001:8, XXREAL_0:2;
hence contradiction by A1, A2, A3, A5, Th19, Th40; :: thesis: verum

end;

hence for m, n being natural odd number st m + 2 < n & n <= len P holds
for e being set holds not e Joins P . m,P . n,G ; :: thesis: verum