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 W1 is Path-like ;
then A4: W2 is Path-like by A1, A2, GLIB_001:182;
not W1 is trivial by A3;
then len W2 <> 1 by A2, GLIB_001:127;
then A5: not W2 is trivial by GLIB_001:127;
W1 is closed by A3;
then W1 .first() = W1 .last() by GLIB_001:def 24;
then W2 .first() = W2 .last() by A2;
then W2 is closed by GLIB_001:def 24;
hence W2 is Cycle-like by A4, A5, GLIB_001:def 31; :: thesis: verum