let G be _Graph; for S being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,S
for W being Walk of G
for V being Walk of H st W = V holds
( W is chordless iff V is chordless )
let S be non empty Subset of (the_Vertices_of G); for H being inducedSubgraph of G,S
for W being Walk of G
for V being Walk of H st W = V holds
( W is chordless iff V is chordless )
let H be inducedSubgraph of G,S; for W being Walk of G
for V being Walk of H st W = V holds
( W is chordless iff V is chordless )
let W be Walk of G; for V being Walk of H st W = V holds
( W is chordless iff V is chordless )
let V be Walk of H; ( W = V implies ( W is chordless iff V is chordless ) )
assume A1:
W = V
; ( W is chordless iff V is chordless )
hereby ( V is chordless implies W is chordless )
assume A2:
W is
chordless
;
not V is chordal assume
V is
chordal
;
contradictionthen consider m,
n being
odd Nat such that A3:
m + 2
< n
and A4:
n <= len V
and A5:
V . m <> V . n
and A6:
ex
e being
object st
e Joins V . m,
V . n,
H
and A7:
for
f being
object st
f in V .edges() holds
not
f Joins V . m,
V . n,
H
;
consider e being
object such that A8:
e Joins V . m,
V . n,
H
by A6;
n in NAT
by ORDINAL1:def 12;
then
V . n in V .vertices()
by A4, GLIB_001:87;
then
V . n in the_Vertices_of H
;
then A9:
V . n in S
by GLIB_000:def 37;
m + 0 <= m + 2
by XREAL_1:7;
then
m <= n
by A3, XXREAL_0:2;
then A10:
m <= len V
by A4, XXREAL_0:2;
m in NAT
by ORDINAL1:def 12;
then
V . m in V .vertices()
by A10, GLIB_001:87;
then
V . m in the_Vertices_of H
;
then A11:
V . m in S
by GLIB_000:def 37;
A12:
for
f being
object st
f in W .edges() holds
not
f Joins W . m,
W . n,
G
proof
let f be
object ;
( f in W .edges() implies not f Joins W . m,W . n,G )
assume
f in W .edges()
;
not f Joins W . m,W . n,G
then A13:
f in V .edges()
by A1, GLIB_001:110;
assume
f Joins W . m,
W . n,
G
;
contradiction
hence
contradiction
by A1, A7, A9, A11, A13, Th19;
verum
end;
e Joins W . m,
W . n,
G
by A1, A8, GLIB_000:72;
hence
contradiction
by A1, A2, A3, A4, A5, A12;
verum
end;
assume A14:
V is chordless
; W is chordless
assume
W is chordal
; contradiction
then consider m, n being odd Nat such that
A15:
m + 2 < n
and
A16:
n <= len W
and
A17:
W . m <> W . n
and
A18:
ex e being object st e Joins W . m,W . n,G
and
A19:
for f being object st f in W .edges() holds
not f Joins W . m,W . n,G
;
consider e being object such that
A20:
e Joins W . m,W . n,G
by A18;
A21:
for f being object st f in V .edges() holds
not f Joins V . m,V . n,H
proof
let f be
object ;
( f in V .edges() implies not f Joins V . m,V . n,H )
assume
f in V .edges()
;
not f Joins V . m,V . n,H
then A22:
f in W .edges()
by A1, GLIB_001:110;
assume
f Joins V . m,
V . n,
H
;
contradiction
then
f Joins W . m,
W . n,
G
by A1, GLIB_000:72;
hence
contradiction
by A19, A22;
verum
end;
n in NAT
by ORDINAL1:def 12;
then
W . n in V .vertices()
by A1, A16, GLIB_001:87;
then
W . n in the_Vertices_of H
;
then A23:
W . n in S
by GLIB_000:def 37;
m + 0 <= m + 2
by XREAL_1:7;
then
m <= n
by A15, XXREAL_0:2;
then A24:
m <= len W
by A16, XXREAL_0:2;
m in NAT
by ORDINAL1:def 12;
then
W . m in V .vertices()
by A1, A24, GLIB_001:87;
then
W . m in the_Vertices_of H
;
then
W . m in S
by GLIB_000:def 37;
then
e Joins V . m,V . n,H
by A1, A20, A23, Th19;
hence
contradiction
by A1, A14, A15, A16, A17, A21; verum