let G2 be _Graph; :: thesis: for E being set
for G1 being reverseEdgeDirections of G2,E
for W2 being Walk of G2
for W1 being Walk of G1 st W1 = W2 holds
( W1 is chordal iff W2 is chordal )
let E be set ; :: thesis: for G1 being reverseEdgeDirections of G2,E
for W2 being Walk of G2
for W1 being Walk of G1 st W1 = W2 holds
( W1 is chordal iff W2 is chordal )
let G1 be reverseEdgeDirections of G2,E; :: thesis: for W2 being Walk of G2
for W1 being Walk of G1 st W1 = W2 holds
( W1 is chordal iff W2 is chordal )
let W2 be Walk of G2; :: thesis: for W1 being Walk of G1 st W1 = W2 holds
( W1 is chordal iff W2 is chordal )
let W1 be Walk of G1; :: thesis: ( W1 = W2 implies ( W1 is chordal iff W2 is chordal ) )
assume A1: W1 = W2 ; :: thesis: ( W1 is chordal iff W2 is chordal )
hence ( W1 is chordal implies W2 is chordal ) by Lm4; :: thesis: ( W2 is chordal implies W1 is chordal )
assume A2: W2 is chordal ; :: thesis: W1 is chordal
reconsider G3 = G2 as reverseEdgeDirections of G1,E by Th3;
reconsider W3 = W2 as Walk of G3 ;
W3 is chordal by A2;
hence W1 is chordal by A1, Lm4; :: thesis: verum