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 E c= the_Edges_of G2 & W1 = W2 & W2 .edges() c= E holds
( W1 is directed iff W2 .reverse() is directed )
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 E c= the_Edges_of G2 & W1 = W2 & W2 .edges() c= E holds
( W1 is directed iff W2 .reverse() is directed )
let G1 be reverseEdgeDirections of G2,E; :: thesis: for W2 being Walk of G2
for W1 being Walk of G1 st E c= the_Edges_of G2 & W1 = W2 & W2 .edges() c= E holds
( W1 is directed iff W2 .reverse() is directed )
let W2 be Walk of G2; :: thesis: for W1 being Walk of G1 st E c= the_Edges_of G2 & W1 = W2 & W2 .edges() c= E holds
( W1 is directed iff W2 .reverse() is directed )
let W1 be Walk of G1; :: thesis: ( E c= the_Edges_of G2 & W1 = W2 & W2 .edges() c= E implies ( W1 is directed iff W2 .reverse() is directed ) )
assume that
A1: E c= the_Edges_of G2 and
A2: W1 = W2 and
A3: W2 .edges() c= E ; :: thesis: ( W1 is directed iff W2 .reverse() is directed )
A4: for n being odd Element of NAT st n < len W2 holds
W2 . (n + 1) in E by A3, GLIB_001:100, TARSKI:def 3;

hereby :: thesis: ( W2 .reverse() is directed implies W1 is directed )

assume W1 is directed ; :: thesis: W2 .reverse() is directed
then A5: for m being odd Element of NAT st m < len W1 holds
W1 . (m + 1) DJoins W1 . m,W1 . (m + 2),G1 by GLIB_001:122;
for n being odd Element of NAT st n < len (W2 .reverse()) holds
(W2 .reverse()) . (n + 1) DJoins (W2 .reverse()) . n,(W2 .reverse()) . (n + 2),G2

proof

let n be odd Element of NAT ; :: thesis: ( n < len (W2 .reverse()) implies (W2 .reverse()) . (n + 1) DJoins (W2 .reverse()) . n,(W2 .reverse()) . (n + 2),G2 )
assume A6: n < len (W2 .reverse()) ; :: thesis: (W2 .reverse()) . (n + 1) DJoins (W2 .reverse()) . n,(W2 .reverse()) . (n + 2),G2
A7: n + 2 <= len (W2 .reverse()) by A6, GLIB_001:1;
A8: 1 <= n by ABIAN:12;
A10: 1 + 0 <= (n + 1) + 1 by XREAL_1:6;
A11: n + 1 <= len (W2 .reverse()) by A6, NAT_1:13;
(n + 2) - (n + 1) <= (len (W2 .reverse())) - (n + 1) by A7, XREAL_1:9;
then (n + 2) - (n + 1) <= (len W2) - (n + 1) by GLIB_001:21;
then reconsider m = ((len W2) - n) - 1 as Element of NAT by INT_1:3;
reconsider m = m as odd Element of NAT ;
( n in dom (W2 .reverse()) & n + 1 in dom (W2 .reverse()) & n + 2 in dom (W2 .reverse()) ) by A6, A7, A8, XREAL_1:6, A10, A11, FINSEQ_3:25;
then a12: ( (W2 .reverse()) . n = W2 . (((len W2) - n) + 1) & ((len W2) - n) + 1 in dom W2 & (W2 .reverse()) . (n + 1) = W2 . (((len W2) - (n + 1)) + 1) & (W2 .reverse()) . (n + 2) = W2 . (((len W2) - (n + 2)) + 1) ) by GLIB_001:25;
then m + 2 <= len W1 by FINSEQ_3:25, A2;
then A13: m < len W1 by GLIB_001:1;
then A14: W1 . (m + 1) in E by A2, A4;
W1 . (m + 1) DJoins W1 . m,W1 . (m + 2),G1 by A5, A13;
hence (W2 .reverse()) . (n + 1) DJoins (W2 .reverse()) . n,(W2 .reverse()) . (n + 2),G2 by A1, A2, a12, A14, Th7; :: thesis: verum

end;

hence W2 .reverse() is directed by GLIB_001:122; :: thesis: verum

end;

assume W2 .reverse() is directed ; :: thesis: W1 is directed
then A15: for m being odd Element of NAT st m < len (W2 .reverse()) holds
(W2 .reverse()) . (m + 1) DJoins (W2 .reverse()) . m,(W2 .reverse()) . (m + 2),G2 by GLIB_001:122;
for n being odd Element of NAT st n < len W1 holds
W1 . (n + 1) DJoins W1 . n,W1 . (n + 2),G1

proof

let n be odd Element of NAT ; :: thesis: ( n < len W1 implies W1 . (n + 1) DJoins W1 . n,W1 . (n + 2),G1 )
assume A16: n < len W1 ; :: thesis: W1 . (n + 1) DJoins W1 . n,W1 . (n + 2),G1
then A17: n < len W2 by A2;
A18: n + 2 <= len W2 by A16, A2, GLIB_001:1;
A19: 1 <= n by ABIAN:12;
A21: 1 + 0 <= (n + 1) + 1 by XREAL_1:6;
A22: n + 1 <= len W2 by NAT_1:13, A2, A16;
(n + 2) - (n + 1) <= (len W2) - (n + 1) by A18, XREAL_1:9;
then reconsider m = ((len W2) - n) - 1 as Element of NAT by INT_1:3;
reconsider m = m as odd Element of NAT ;
( n in dom W2 & n + 1 in dom W2 & n + 2 in dom W2 ) by A2, A16, A18, A19, XREAL_1:6, A21, A22, FINSEQ_3:25;
then a23: ( W2 . n = (W2 .reverse()) . (((len W2) - n) + 1) & ((len W2) - n) + 1 in dom (W2 .reverse()) & W2 . (n + 1) = (W2 .reverse()) . (((len W2) - (n + 1)) + 1) & W2 . (n + 2) = (W2 .reverse()) . (((len W2) - (n + 2)) + 1) ) by GLIB_001:24;
then A23: ( W1 . n = (W2 .reverse()) . (m + 2) & m + 2 in dom (W2 .reverse()) & W1 . (n + 1) = (W2 .reverse()) . (m + 1) & W1 . (n + 2) = (W2 .reverse()) . m ) by A2;
m + 2 <= len (W2 .reverse()) by a23, FINSEQ_3:25;
then A24: m < len (W2 .reverse()) by GLIB_001:1;
A25: W1 . (n + 1) in E by A17, A2, A4;
W1 . (n + 1) DJoins W1 . (n + 2),W1 . n,G2 by A23, A15, A24;
hence W1 . (n + 1) DJoins W1 . n,W1 . (n + 2),G1 by A1, A25, Th7; :: thesis: verum

end;

hence W1 is directed by GLIB_001:122; :: thesis: verum