theorem Th151: :: GLIB_006:147

for G2 being _Graph
for v1, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2
for T being Trail of G1 st not e in the_Edges_of G2 & T .first() in the_Vertices_of G2 & T .last() in the_Vertices_of G2 holds
not e in T .edges()