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

for e being object holds not e Joins P . m,P . n,G ; :: thesis: verum

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

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

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;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

for e being object holds not e Joins P . m,P . n,G ; :: thesis: verum