let G2 be _Graph; :: thesis:
let v1, v2 be Vertex of G2; :: thesis:
let e be object ; :: thesis:
let G1 be addEdge of G2,v1,e,v2; :: thesis:
assume that
A1: not e in the_Edges_of G2 and
A2: ex e2 being object st e2 DJoins v1,v2,G2 ; :: thesis:
ex e1, e2, u1, u2 being object st
( e1 DJoins u1,u2,G1 & e2 DJoins u1,u2,G1 & e1 <> e2 )

consider e2 being object such that
A3: e2 DJoins v1,v2,G2 by A2;
take e ; :: thesis:
take e2 ; :: thesis:
take v1 ; :: thesis:
take v2 ; :: thesis:
thus e DJoins v1,v2,G1 by A1, Th109; :: thesis:
thus e2 DJoins v1,v2,G1 by A3, Th74; :: thesis:
thus e <> e2 by A1, A3, GLIB_000:def 14; :: thesis:

end;