let G1 be _Graph; :: thesis: for G2 being removeLoops of G1 holds

( G1 is chordal iff G2 is chordal )

let G2 be removeLoops of G1; :: thesis: ( G1 is chordal iff G2 is chordal )

( G1 is chordal iff G2 is chordal )

let G2 be removeLoops of G1; :: thesis: ( G1 is chordal iff G2 is chordal )

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

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

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

P2 is chordal

hence
G2 is chordal
by CHORD:def 11; :: thesis: verumP2 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

end;assume A2: ( P2 .length() > 3 & P2 is Cycle-like ) ; :: thesis: P2 is chordal

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

hence
P2 is chordal
by CHORD:def 10; :: thesis: verum( 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 ) )

reconsider P1 = P2 as Walk of G1 by GLIB_001:167;

( P1 .length() > 3 & P1 is Cycle-like ) by A2, GLIB_001:114, GLIB_006:24;

then consider m, n being odd Nat such that

A3: ( m + 2 < n & n <= len P1 & P1 . m <> P1 . n ) and

A4: ex e being object st e Joins P1 . m,P1 . n,G1 and

A5: for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1 by A1, CHORD:def 11, CHORD:def 10;

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 A3; :: 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 ) )

assume f in P2 .edges() ; :: thesis: not f Joins P2 . m,P2 . n,G2

then f in P1 .edges() by GLIB_001:110;

hence not f Joins P2 . m,P2 . n,G2 by A5, GLIB_000:72; :: thesis: verum

end;( P1 .length() > 3 & P1 is Cycle-like ) by A2, GLIB_001:114, GLIB_006:24;

then consider m, n being odd Nat such that

A3: ( m + 2 < n & n <= len P1 & P1 . m <> P1 . n ) and

A4: ex e being object st e Joins P1 . m,P1 . n,G1 and

A5: for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1 by A1, CHORD:def 11, CHORD:def 10;

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 A3; :: 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 ) )

hereby :: thesis: for f being object st f in P2 .edges() holds

not f Joins P2 . m,P2 . n,G2

let f be object ; :: thesis: ( f in P2 .edges() implies not f Joins P2 . m,P2 . n,G2 )not f Joins P2 . m,P2 . n,G2

consider e being object such that

A6: e Joins P1 . m,P1 . n,G1 by A4;

take e = e; :: thesis: e Joins P2 . m,P2 . n,G2

A7: e in the_Edges_of G1 by A6, GLIB_000:def 13;

not e in G1 .loops() by A3, A6, Th46;

then e in (the_Edges_of G1) \ (G1 .loops()) by A7, XBOOLE_0:def 5;

then e in the_Edges_of G2 by GLIB_000:53;

hence e Joins P2 . m,P2 . n,G2 by A6, GLIB_000:73; :: thesis: verum

end;A6: e Joins P1 . m,P1 . n,G1 by A4;

take e = e; :: thesis: e Joins P2 . m,P2 . n,G2

A7: e in the_Edges_of G1 by A6, GLIB_000:def 13;

not e in G1 .loops() by A3, A6, Th46;

then e in (the_Edges_of G1) \ (G1 .loops()) by A7, XBOOLE_0:def 5;

then e in the_Edges_of G2 by GLIB_000:53;

hence e Joins P2 . m,P2 . n,G2 by A6, GLIB_000:73; :: thesis: verum

assume f in P2 .edges() ; :: thesis: not f Joins P2 . m,P2 . n,G2

then f in P1 .edges() by GLIB_001:110;

hence not f Joins P2 . m,P2 . n,G2 by A5, GLIB_000:72; :: thesis: verum

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

P1 is chordal

hence
G1 is chordal
by CHORD:def 11; :: thesis: verumP1 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

end;assume A9: ( P1 .length() > 3 & P1 is Cycle-like ) ; :: thesis: P1 is chordal

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

hence
P1 is chordal
by CHORD:def 10; :: thesis: verum( 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 ) )

P1 .edges() misses G1 .loops()

then A11: P1 .edges() c= the_Edges_of G2 by GLIB_000:53;

the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:53;

then P1 .vertices() c= the_Vertices_of G2 ;

then reconsider P2 = P1 as Walk of G2 by A11, GLIB_001:170;

( P2 .length() > 3 & P2 is Cycle-like ) by A9, GLIB_001:114, GLIB_006:24;

then 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, CHORD:def 11, CHORD:def 10;

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 by A13, GLIB_000:72; :: thesis: for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1

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 A15: 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 A15, GLIB_000:73; :: thesis: verum

end;proof

then
P1 .edges() c= (the_Edges_of G1) \ (G1 .loops())
by XBOOLE_1:86;
assume
P1 .edges() meets G1 .loops()
; :: thesis: contradiction

then consider v, e being object such that

A10: ( e Joins v,v,G1 & P1 = G1 .walkOf (v,e,v) ) by A9, Th57;

(2 * (P1 .length())) + 1 = len P1 by GLIB_001:112

.= (2 * 1) + 1 by A10, GLIB_001:14 ;

hence contradiction by A9; :: thesis: verum

end;then consider v, e being object such that

A10: ( e Joins v,v,G1 & P1 = G1 .walkOf (v,e,v) ) by A9, Th57;

(2 * (P1 .length())) + 1 = len P1 by GLIB_001:112

.= (2 * 1) + 1 by A10, GLIB_001:14 ;

hence contradiction by A9; :: thesis: verum

then A11: P1 .edges() c= the_Edges_of G2 by GLIB_000:53;

the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:53;

then P1 .vertices() c= the_Vertices_of G2 ;

then reconsider P2 = P1 as Walk of G2 by A11, GLIB_001:170;

( P2 .length() > 3 & P2 is Cycle-like ) by A9, GLIB_001:114, GLIB_006:24;

then 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, CHORD:def 11, CHORD:def 10;

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 by A13, GLIB_000:72; :: thesis: for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1

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 A15: 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 A15, GLIB_000:73; :: thesis: verum