let G1 be _Graph; :: thesis: for G2 being SimpleGraph 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 SimpleGraph 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()
consider H being removeParallelEdges of G1 such that
A1: G2 is removeLoops of H by Th119;
consider W2 being Walk of H such that
A2: W2 is_Walk_from W1 .first() ,W1 .last() by Lm4;
consider W3 being Walk of G2 such that
A3: W3 is_Walk_from W2 .first() ,W2 .last() by A1, Th61;
take W3 ; :: thesis: W3 is_Walk_from W1 .first() ,W1 .last()
( W1 .first() = W2 .first() & W1 .last() = W2 .last() ) by A2, GLIB_001:def 23;
hence W3 is_Walk_from W1 .first() ,W1 .last() by A3; :: thesis: verum