let G2 be _Graph; for V being set
for G1 being addVertices of G2,V holds
( G2 is chordal iff G1 is chordal )
let V be set ; for G1 being addVertices of G2,V holds
( G2 is chordal iff G1 is chordal )
let G1 be addVertices of G2,V; ( G2 is chordal iff G1 is chordal )
thus
( G2 is chordal implies G1 is chordal )
( G1 is chordal implies G2 is chordal )proof
assume A1:
G2 is
chordal
;
G1 is chordal
for
P being
Walk of
G1 st
P .length() > 3 &
P is
Cycle-like holds
P is
chordal
proof
let P be
Walk of
G1;
( P .length() > 3 & P is Cycle-like implies P is chordal )
assume A2:
(
P .length() > 3 &
P is
Cycle-like )
;
P is chordal
per cases
( P .vertices() misses V \ (the_Vertices_of G2) or not P is V5() )
by Th94;
suppose
P .vertices() misses V \ (the_Vertices_of G2)
;
P is chordal then reconsider W =
P as
Walk of
G2 by Th95;
A3:
W is
Cycle-like
by A2, Th80;
P .length() = W .length()
by GLIB_001:114;
then
W is
chordal
by A1, A2, A3, CHORD:def 11;
then consider m,
n being
odd Nat such that A4:
(
m + 2
< n &
n <= len W &
W . m <> W . n )
and A5:
ex
e being
object st
e Joins W . m,
W . n,
G2
and A6:
for
f being
object st
f in W .edges() holds
not
f Joins W . m,
W . n,
G2
by CHORD:def 10;
now ex m, n being odd Nat st
( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )take m =
m;
ex n being odd Nat st
( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )take n =
n;
( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )thus
(
m + 2
< n &
n <= len P &
P . m <> P . n )
by A4;
( ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )thus
ex
e being
object st
e Joins P . m,
P . n,
G1
by A5, Th74;
for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1thus
for
f being
object st
f in P .edges() holds
not
f Joins P . m,
P . n,
G1
verum end; hence
P is
chordal
by CHORD:def 10;
verum end; end;
end;
hence
G1 is
chordal
by CHORD:def 11;
verum
end;
assume A10:
G1 is chordal
; G2 is chordal
G2 is inducedSubgraph of G1,(the_Vertices_of G2)
by Th88;
hence
G2 is chordal
by A10; verum