let G2 be _Graph; :: thesis:
let v be object ; :: thesis:
let V be set ; :: thesis:
let G1 be addAdjVertexAll of G2,v,V; :: thesis:
let v1 be Vertex of G1; :: thesis:
let v2 be Vertex of G2; :: thesis:
assume A1: ( v1 = v2 & not v2 in V ) ; :: thesis:

suppose A2: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis:

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

let e be object ; :: thesis:
A5: e is set by TARSKI:1;
assume e in v1 .edgesIn() ; :: thesis:
then consider x being set such that
A6: e DJoins x,v1,G1 by GLIB_000:57;
A7: x <> v

assume x = v ; :: thesis:
then e Joins v1,v,G1 by A6, GLIB_000:16;
hence contradiction by A1, A2, GLIB_007:def 4; :: thesis:

end;

v1 <> v by A1, A2;
then e DJoins x,v1,G2 by A2, A6, A7, GLIB_007:def 4;
hence e in v2 .edgesIn() by A1, A5, 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 e be object ; :: thesis:
A10: e is set by TARSKI:1;
assume e in v1 .edgesOut() ; :: thesis:
then consider x being set such that
A11: e DJoins v1,x,G1 by GLIB_000:59;
A12: x <> v

assume x = v ; :: thesis:
then e Joins v1,v,G1 by A11, GLIB_000:16;
hence contradiction by A1, A2, GLIB_007:def 4; :: thesis:

end;

v1 <> v by A1, A2;
then e DJoins v1,x,G2 by A2, A11, A12, GLIB_007:def 4;
hence e in v2 .edgesOut() by A1, A10, 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 c= the_Vertices_of G2 or v in the_Vertices_of G2 ) ; :: thesis:

then G1 == G2 by GLIB_007:def 4;
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;