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