let G2 be _Graph; :: thesis: for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, v2 being object holds
( ex W1 being Walk of G1 st W1 is_Walk_from v1,v2 iff ex W2 being Walk of G2 st W2 is_Walk_from v1,v2 )
let E be set ; :: thesis: for G1 being reverseEdgeDirections of G2,E
for v1, v2 being object holds
( ex W1 being Walk of G1 st W1 is_Walk_from v1,v2 iff ex W2 being Walk of G2 st W2 is_Walk_from v1,v2 )
let G1 be reverseEdgeDirections of G2,E; :: thesis: for v1, v2 being object holds
( ex W1 being Walk of G1 st W1 is_Walk_from v1,v2 iff ex W2 being Walk of G2 st W2 is_Walk_from v1,v2 )
let v1, v2 be object ; :: thesis: ( ex W1 being Walk of G1 st W1 is_Walk_from v1,v2 iff ex W2 being Walk of G2 st W2 is_Walk_from v1,v2 )

hereby :: thesis: ( ex W2 being Walk of G2 st W2 is_Walk_from v1,v2 implies ex W1 being Walk of G1 st W1 is_Walk_from v1,v2 )

given W1 being Walk of G1 such that A1: W1 is_Walk_from v1,v2 ; :: thesis: ex W2 being Walk of G2 st W2 is_Walk_from v1,v2
reconsider W2 = W1 as Walk of G2 by Th15;
take W2 = W2; :: thesis: W2 is_Walk_from v1,v2
thus W2 is_Walk_from v1,v2 by A1, GLIB_001:19; :: thesis: verum

end;

given W2 being Walk of G2 such that A2: W2 is_Walk_from v1,v2 ; :: thesis: ex W1 being Walk of G1 st W1 is_Walk_from v1,v2
reconsider W1 = W2 as Walk of G1 by Th14;
take W1 ; :: thesis: W1 is_Walk_from v1,v2
thus W1 is_Walk_from v1,v2 by A2, GLIB_001:19; :: thesis: verum