let G1 be _Graph; :: thesis: for G2 being DSimpleGraph of G1

for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

let G2 be DSimpleGraph of G1; :: thesis: for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

let W1 be Walk of G1; :: thesis: ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

set G3 = the SimpleGraph of G2;

the SimpleGraph of G2 is SimpleGraph of G1 by Th133;

then consider W3 being Walk of the SimpleGraph of G2 such that

A1: W3 is_Walk_from W1 .first() ,W1 .last() by Th136;

reconsider W2 = W3 as Walk of G2 by GLIB_001:167;

take W2 ; :: thesis: W2 is_Walk_from W1 .first() ,W1 .last()

thus W2 is_Walk_from W1 .first() ,W1 .last() by A1, GLIB_001:19; :: thesis: verum

for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

let G2 be DSimpleGraph of G1; :: thesis: for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

let W1 be Walk of G1; :: thesis: ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

set G3 = the SimpleGraph of G2;

the SimpleGraph of G2 is SimpleGraph of G1 by Th133;

then consider W3 being Walk of the SimpleGraph of G2 such that

A1: W3 is_Walk_from W1 .first() ,W1 .last() by Th136;

reconsider W2 = W3 as Walk of G2 by GLIB_001:167;

take W2 ; :: thesis: W2 is_Walk_from W1 .first() ,W1 .last()

thus W2 is_Walk_from W1 .first() ,W1 .last() by A1, GLIB_001:19; :: thesis: verum