let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is Trail-like holds
W2 is Trail-like
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 & W1 is Trail-like holds
W2 is Trail-like
let W2 be Walk of G2; :: thesis: ( W1 = W2 & W1 is Trail-like implies W2 is Trail-like )
assume W1 = W2 ; :: thesis: ( not W1 is Trail-like or W2 is Trail-like )
then A2: W1 .edgeSeq() = W2 .edgeSeq() by GLIB_001:86;
assume W1 is Trail-like ; :: thesis: W2 is Trail-like
then W2 .edgeSeq() is one-to-one by A2, GLIB_001:def 27;
hence W2 is Trail-like by GLIB_001:def 27; :: thesis: verum