theorem :: GLIB_001:142

for G being _Graph
for W being Trail of G
for e being set st e in (W .last()) .edgesInOut() & not e in W .edges() holds
W .addEdge e is Trail-like by Lm60;