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

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