let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is Cycle-like holds
W2 is Cycle-like )
assume A1: G1 == G2 ; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is Cycle-like holds
W2 is Cycle-like
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 & W1 is Cycle-like holds
W2 is Cycle-like
let W2 be Walk of G2; :: thesis: ( W1 = W2 & W1 is Cycle-like implies W2 is Cycle-like )
assume A2: W1 = W2 ; :: thesis: ( not W1 is Cycle-like or W2 is Cycle-like )
assume A3: W1 is Cycle-like ; :: thesis: W2 is Cycle-like
then len W2 <> 1 by A2, GLIB_001:126;
then A4: not W2 is trivial by GLIB_001:126;
W1 .first() = W1 .last() by A3, GLIB_001:def 24;
then W2 .first() = W2 .last() by A2;
then A5: W2 is closed by GLIB_001:def 24;
W2 is Path-like by A1, A2, A3, GLIB_001:181;
hence W2 is Cycle-like by A4, A5, GLIB_001:def 31; :: thesis: verum