let G2 be _Graph; :: thesis: 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()
let v1, e, v2 be object ; :: thesis: 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()
let G1 be addAdjVertex of G2,v1,e,v2; :: thesis: 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()
let T be Trail of G1; :: thesis: ( not e in the_Edges_of G2 & T .first() in the_Vertices_of G2 & T .last() in the_Vertices_of G2 implies not e in T .edges() )
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: not e in T .edges()

per cases ( ( v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 ) or ( not v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 ) or ( ( 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 ) ) ) ;

suppose A3: ( v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 ) ; :: thesis: not e in T .edges()

per cases ( v2 in T .vertices() or not v2 in T .vertices() ) ;

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

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: verum

end;

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

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: verum

end;

end;

end;

suppose A6: ( not v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 ) ; :: thesis: not e in T .edges()

per cases ( v1 in T .vertices() or not v1 in T .vertices() ) ;

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

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: verum

end;

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

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: verum

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: not e in T .edges()

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: verum

end;

end;