let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is Path-like holds
W2 is Path-like
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 & W1 is Path-like holds
W2 is Path-like
let W2 be Walk of G2; :: thesis: ( W1 = W2 & W1 is Path-like implies W2 is Path-like )
assume A1: W1 = W2 ; :: thesis: ( not W1 is Path-like or W2 is Path-like )
assume W1 is Path-like ; :: thesis: W2 is Path-like
then ( W2 is Trail-like & ( for m, n being odd Element of NAT st m < n & n <= len W2 & W2 . m = W2 . n holds
( m = 1 & n = len W2 ) ) ) by A1, Th26, GLIB_001:def 28;
hence W2 is Path-like by GLIB_001:def 28; :: thesis: verum