let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1

for W2 being Walk of G2 st W1 = W2 & W1 is trivial holds

W2 is trivial

let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 & W1 is trivial holds

W2 is trivial

let W2 be Walk of G2; :: thesis: ( W1 = W2 & W1 is trivial implies W2 is trivial )

assume that

A1: W1 = W2 and

A2: W1 is trivial ; :: thesis: W2 is trivial

len W2 = 1 by A1, A2, Lm55;

hence W2 is trivial by Lm55; :: thesis: verum

for W2 being Walk of G2 st W1 = W2 & W1 is trivial holds

W2 is trivial

let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 & W1 is trivial holds

W2 is trivial

let W2 be Walk of G2; :: thesis: ( W1 = W2 & W1 is trivial implies W2 is trivial )

assume that

A1: W1 = W2 and

A2: W1 is trivial ; :: thesis: W2 is trivial

len W2 = 1 by A1, A2, Lm55;

hence W2 is trivial by Lm55; :: thesis: verum