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