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

( G1 is chordal iff G2 is chordal )

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

consider H being removeDParallelEdges of G1 such that

A1: G2 is removeLoops of H by Th120;

( H is chordal iff G2 is chordal ) by A1, Th65;

hence ( G1 is chordal iff G2 is chordal ) by Th107; :: thesis: verum

( G1 is chordal iff G2 is chordal )

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

consider H being removeDParallelEdges of G1 such that

A1: G2 is removeLoops of H by Th120;

( H is chordal iff G2 is chordal ) by A1, Th65;

hence ( G1 is chordal iff G2 is chordal ) by Th107; :: thesis: verum