:: deftheorem Def10 defines .append GLIB_001:def 10 :
for G being _Graph
for W1, W2 being Walk of G holds
( ( W1 .last() = W2 .first() implies W1 .append W2 = W1 ^' W2 ) & ( not W1 .last() = W2 .first() implies W1 .append W2 = W1 ) );