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 odd Nat st m + 2 < n & n <= len W holds
for e being object 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 odd Nat st m + 2 < n & n <= len W holds
for e being object 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 odd Nat st m + 2 < n & n <= len W holds
for e being object holds not e Joins W . m,W . n,G
let P be Walk of GA; :: thesis: ( P is minlength implies for m, n being odd Nat st m + 2 < n & n <= len P holds
for e being object holds not e Joins P . m,P . n,G )
A1: S = the_Vertices_of GA by GLIB_000:def 37;
assume A2: P is minlength ; :: thesis: for m, n being odd Nat st m + 2 < n & n <= len P holds
for e being object holds not e Joins P . m,P . n,G

now :: thesis: for m, n being odd Nat st m + 2 < n & n <= len P holds
for e being object holds not e Joins P . m,P . n,G

let m, n be odd Nat; :: thesis: ( m + 2 < n & n <= len P implies for e being object holds not e Joins P . m,P . n,G )
assume that
A3: m + 2 < n and
A4: n <= len P ; :: thesis: for e being object holds not e Joins P . m,P . n,G
m + 0 <= m + 2 by XREAL_1:7;
then A5: m <= n by A3, XXREAL_0:2;
n in NAT by ORDINAL1:def 12;
then A6: P . n in the_Vertices_of GA by A4, GLIB_001:7;
m in NAT by ORDINAL1:def 12;
then A7: P . m in the_Vertices_of GA by A4, A5, GLIB_001:7, XXREAL_0:2;
let e be object ; :: thesis: not e Joins P . m,P . n,G
assume e Joins P . m,P . n,G ; :: thesis: contradiction
hence contradiction by A2, A1, A3, A4, A7, A6, Th19, Th39; :: thesis: verum

end;

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