let G2 be _Graph; :: thesis: for V being set
for G1 being addLoops of G2,V holds
( G1 is chordal iff G2 is chordal )
let V be set ; :: thesis: for G1 being addLoops of G2,V holds
( G1 is chordal iff G2 is chordal )
let G1 be addLoops of G2,V; :: thesis: ( G1 is chordal iff G2 is chordal )

hereby :: thesis: ( G2 is chordal implies G1 is chordal )

assume A1: G1 is chordal ; :: thesis: G2 is chordal

now :: thesis: for P2 being Walk of G2 st P2 .length() > 3 & P2 is Cycle-like holds
P2 is chordal

let P2 be Walk of G2; :: thesis: ( P2 .length() > 3 & P2 is Cycle-like implies P2 is chordal )
assume A2: ( P2 .length() > 3 & P2 is Cycle-like ) ; :: thesis: P2 is chordal
reconsider P1 = P2 as Walk of G1 by GLIB_006:75;
A3: ( P1 .length() = P2 .length() & P1 is Cycle-like ) by A2, GLIB_006:76, GLIB_001:114;

now :: thesis: ex m, n being odd Nat st
( m + 2 < n & n <= len P2 & P2 . m <> P2 . n & ex e being object st e Joins P2 . m,P2 . n,G2 & ( for f being object st f in P2 .edges() holds
not f Joins P2 . m,P2 . n,G2 ) )

consider m, n being odd Nat such that
A4: ( m + 2 < n & n <= len P1 & P1 . m <> P1 . n ) and
A5: ex e being object st e Joins P1 . m,P1 . n,G1 and
A6: for f being object st f in P1 .edges() holds
not f Joins P1 . m,P1 . n,G1 by A1, A2, A3, CHORD:def 10, CHORD:def 11;
take m = m; :: thesis: ex n being odd Nat st
( m + 2 < n & n <= len P2 & P2 . m <> P2 . n & ex e being object st e Joins P2 . m,P2 . n,G2 & ( for f being object st f in P2 .edges() holds
not f Joins P2 . m,P2 . n,G2 ) )
take n = n; :: thesis: ( m + 2 < n & n <= len P2 & P2 . m <> P2 . n & ex e being object st e Joins P2 . m,P2 . n,G2 & ( for f being object st f in P2 .edges() holds
not f Joins P2 . m,P2 . n,G2 ) )
thus ( m + 2 < n & n <= len P2 & P2 . m <> P2 . n ) by A4; :: thesis: ( ex e being object st e Joins P2 . m,P2 . n,G2 & ( for f being object st f in P2 .edges() holds
not f Joins P2 . m,P2 . n,G2 ) )
thus ex e being object st e Joins P2 . m,P2 . n,G2 :: thesis: for f being object st f in P2 .edges() holds
not f Joins P2 . m,P2 . n,G2

proof

consider e being object such that
A7: e Joins P1 . m,P1 . n,G1 by A5;
take e ; :: thesis: e Joins P2 . m,P2 . n,G2
thus e Joins P2 . m,P2 . n,G2 by A4, A7, Th17; :: thesis: verum

end;

thus for f being object st f in P2 .edges() holds
not f Joins P2 . m,P2 . n,G2 :: thesis: verum

proof

let f be object ; :: thesis: ( f in P2 .edges() implies not f Joins P2 . m,P2 . n,G2 )
assume f in P2 .edges() ; :: thesis: not f Joins P2 . m,P2 . n,G2
then f in P1 .edges() by GLIB_001:110;
then not f Joins P1 . m,P1 . n,G1 by A6;
hence not f Joins P2 . m,P2 . n,G2 by A4, Th17; :: thesis: verum

end;

end;

hence P2 is chordal by CHORD:def 10; :: thesis: verum

end;

hence G2 is chordal by CHORD:def 11; :: thesis: verum

end;

assume A8: G2 is chordal ; :: thesis: G1 is chordal

now :: thesis: for P1 being Walk of G1 st P1 .length() > 3 & P1 is Cycle-like holds
P1 is chordal

let P1 be Walk of G1; :: thesis: ( P1 .length() > 3 & P1 is Cycle-like implies P1 is chordal )
assume A9: ( P1 .length() > 3 & P1 is Cycle-like ) ; :: thesis: P1 is chordal
P1 is Walk of G2

proof

assume P1 is not Walk of G2 ; :: thesis: contradiction
then consider v, e being object such that
A10: ( e Joins v,v,G1 & P1 = G1 .walkOf (v,e,v) ) by A9, Th37;
(2 * 1) + 1 = len P1 by A10, GLIB_001:14
.= (2 * (P1 .length())) + 1 by GLIB_001:112 ;
hence contradiction by A9; :: thesis: verum

end;

then reconsider P2 = P1 as Walk of G2 ;
A11: ( P1 .length() = P2 .length() & P2 is Cycle-like ) by A9, GLIB_006:76, GLIB_001:114;

now :: thesis: ex m, n being odd Nat st
( m + 2 < n & n <= len P1 & P1 . m <> P1 . n & ex e being object st e Joins P1 . m,P1 . n,G1 & ( for f being object st f in P1 .edges() holds
not f Joins P1 . m,P1 . n,G1 ) )

consider m, n being odd Nat such that
A12: ( m + 2 < n & n <= len P2 & P2 . m <> P2 . n ) and
A13: ex e being object st e Joins P2 . m,P2 . n,G2 and
A14: for f being object st f in P2 .edges() holds
not f Joins P2 . m,P2 . n,G2 by A8, A9, A11, CHORD:def 10, CHORD:def 11;
take m = m; :: thesis: ex n being odd Nat st
( m + 2 < n & n <= len P1 & P1 . m <> P1 . n & ex e being object st e Joins P1 . m,P1 . n,G1 & ( for f being object st f in P1 .edges() holds
not f Joins P1 . m,P1 . n,G1 ) )
take n = n; :: thesis: ( m + 2 < n & n <= len P1 & P1 . m <> P1 . n & ex e being object st e Joins P1 . m,P1 . n,G1 & ( for f being object st f in P1 .edges() holds
not f Joins P1 . m,P1 . n,G1 ) )
thus ( m + 2 < n & n <= len P1 & P1 . m <> P1 . n ) by A12; :: thesis: ( ex e being object st e Joins P1 . m,P1 . n,G1 & ( for f being object st f in P1 .edges() holds
not f Joins P1 . m,P1 . n,G1 ) )
thus ex e being object st e Joins P1 . m,P1 . n,G1 :: thesis: for f being object st f in P1 .edges() holds
not f Joins P1 . m,P1 . n,G1

proof

consider e being object such that
A15: e Joins P2 . m,P2 . n,G2 by A13;
take e ; :: thesis: e Joins P1 . m,P1 . n,G1
thus e Joins P1 . m,P1 . n,G1 by A12, A15, Th17; :: thesis: verum

end;

thus for f being object st f in P1 .edges() holds
not f Joins P1 . m,P1 . n,G1 :: thesis: verum

proof

let f be object ; :: thesis: ( f in P1 .edges() implies not f Joins P1 . m,P1 . n,G1 )
assume f in P1 .edges() ; :: thesis: not f Joins P1 . m,P1 . n,G1
then f in P2 .edges() by GLIB_001:110;
then not f Joins P2 . m,P2 . n,G2 by A14;
hence not f Joins P1 . m,P1 . n,G1 by A12, Th17; :: thesis: verum

end;

end;

hence P1 is chordal by CHORD:def 10; :: thesis: verum

end;

hence G1 is chordal by CHORD:def 11; :: thesis: verum