let G1 be reverseEdgeDirections of G,E; :: thesis: G1 is chordal
for W1 being Walk of G1 st W1 .length() > 3 & W1 is Cycle-like holds
W1 is chordal

proof

let W1 be Walk of G1; :: thesis: ( W1 .length() > 3 & W1 is Cycle-like implies W1 is chordal )
reconsider W = W1 as Walk of G by Th15;
assume ( W1 .length() > 3 & W1 is Cycle-like ) ; :: thesis: W1 is chordal
then ( W .length() > 3 & W is Cycle-like ) by GLIB_006:24, GLIB_001:114;
then W is chordal by CHORD:def 11;
hence W1 is chordal by Th18; :: thesis: verum

end;

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