let G1, G2 be _Graph; :: thesis: ( G1 == G2 & G1 is chordal implies G2 is chordal )
assume A1: G1 == G2 ; :: thesis: ( not G1 is chordal or G2 is chordal )
assume A2: G1 is chordal ; :: thesis: G2 is chordal

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

let W be Walk of G2; :: thesis: ( W .length() > 3 & W is Cycle-like implies W is chordal )
assume that
A3: W .length() > 3 and
A4: W is Cycle-like ; :: thesis: W is chordal
reconsider W2 = W as Walk of G1 by A1, GLIB_001:179;
(2 * (W2 .length())) + 1 = len W by GLIB_001:112;
then A5: (2 * (W2 .length())) + 1 = (2 * (W .length())) + 1 by GLIB_001:112;
W2 is Cycle-like by A4, Th24;
then W2 is chordal by A2, A3, A5;
hence W is chordal by A1, Th85; :: thesis: verum

end;

hence G2 is chordal ; :: thesis: verum