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

( G1 is chordal iff G2 is chordal )

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

consider H being removeParallelEdges of G1 such that

A1: G2 is removeLoops of H by Th119;

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

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

( G1 is chordal iff G2 is chordal )

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

consider H being removeParallelEdges of G1 such that

A1: G2 is removeLoops of H by Th119;

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

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