let G2 be _Graph; :: thesis:
let v1, e, v2 be object ; :: thesis:
let G1 be addAdjVertex of G2,v1,e,v2; :: thesis:
let T be Trail of G1; :: thesis:
assume that
A1: not e in the_Edges_of G2 and
A2: ( T .first() in the_Vertices_of G2 & T .last() in the_Vertices_of G2 ) ; :: thesis:

per cases ;

suppose A3: ( v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 ) ; :: thesis:

per cases ;

suppose A4: v2 in T .vertices() ; :: thesis:

reconsider w = v2 as Vertex of G1 by A1, A3, Th133;
w is endvertex by A1, A3, Th145;
hence not e in T .edges() by A2, A3, A4, GLIB_001:143; :: thesis:

end;

suppose not v2 in T .vertices() ; :: thesis:

then reconsider W = T as Walk of G2 by A1, A3, Th149;
not e in W .edges() by A1;
hence not e in T .edges() by GLIB_001:110; :: thesis:

end;

end;

end;

suppose A6: ( not v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 ) ; :: thesis:

per cases ;

suppose A7: v1 in T .vertices() ; :: thesis:

reconsider w = v1 as Vertex of G1 by A1, A6, Th134;
w is endvertex by A1, A6, Th146;
hence not e in T .edges() by A2, A6, A7, GLIB_001:143; :: thesis:

end;

suppose not v1 in T .vertices() ; :: thesis:

then reconsider W = T as Walk of G2 by A1, A6, Th150;
not e in W .edges() by A1;
hence not e in T .edges() by GLIB_001:110; :: thesis:

end;

end;

end;

suppose ( ( not v1 in the_Vertices_of G2 or v2 in the_Vertices_of G2 ) & ( v1 in the_Vertices_of G2 or not v2 in the_Vertices_of G2 ) ) ; :: thesis:

then G1 == G2 by Def12;
then not e in the_Edges_of G1 by A1, GLIB_000:def 34;
hence not e in T .edges() ; :: thesis:

end;

end;