let G2 be _Graph; :: thesis:
let v, w, e be object ; :: thesis:
let G1 be addEdge of G2,v,e,w; :: thesis:
let v1 be Vertex of G1; :: thesis:
let v2 be Vertex of G2; :: thesis:
assume A1: ( v1 = v2 & v2 <> v & v2 <> w ) ; :: thesis:

suppose A2: ( v in the_Vertices_of G2 & w in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis:

A3: G2 is Subgraph of G1 by GLIB_006:57;
A4: v2 .edgesIn() c= v1 .edgesIn() by A1, A3, GLIB_000:78;

let f be object ; :: thesis:
assume f in v1 .edgesIn() ; :: thesis:
then consider x being set such that
A5: f DJoins x,v1,G1 by GLIB_000:57;
f in the_Edges_of G2

assume A7: not f in the_Edges_of G2 ; :: thesis:
f Joins x,v1,G1 by A5, GLIB_000:16;
hence contradiction by A1, A2, A7, GLIB_006:107; :: thesis:

end;

hence f in v2 .edgesIn() by A1, A5, GLIB_006:71, GLIB_000:57; :: thesis:

end;

then v1 .edgesIn() c= v2 .edgesIn() by TARSKI:def 3;
hence A8: v1 .edgesIn() = v2 .edgesIn() by A4, XBOOLE_0:def 10; :: thesis:
hence v1 .inDegree() = v2 .inDegree() ; :: thesis:
A9: v2 .edgesOut() c= v1 .edgesOut() by A1, A3, GLIB_000:78;

let f be object ; :: thesis:
assume f in v1 .edgesOut() ; :: thesis:
then consider x being set such that
A10: f DJoins v1,x,G1 by GLIB_000:59;
f in the_Edges_of G2

assume A12: not f in the_Edges_of G2 ; :: thesis:
f Joins x,v1,G1 by A10, GLIB_000:16;
hence contradiction by A1, A2, A12, GLIB_006:107; :: thesis:

end;

hence f in v2 .edgesOut() by A1, A10, GLIB_006:71, GLIB_000:59; :: thesis:

end;

then v1 .edgesOut() c= v2 .edgesOut() by TARSKI:def 3;
hence A13: v1 .edgesOut() = v2 .edgesOut() by A9, XBOOLE_0:def 10; :: thesis:
hence v1 .outDegree() = v2 .outDegree() ; :: thesis:
thus ( v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() ) by A8, A13; :: thesis:

end;

suppose ( not v in the_Vertices_of G2 or not w in the_Vertices_of G2 or e in the_Edges_of G2 ) ; :: thesis:

then G1 == G2 by GLIB_006:def 11;
hence ( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() ) by A1, GLIB_000:96; :: thesis:

end;

end;