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 ; :: thesis:

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

then consider E being set such that
A3: ( card V = card E & E misses the_Edges_of G2 ) and
the_Edges_of G1 = (the_Edges_of G2) \/ E and
A4: for v3 being object st v3 in V holds
ex e1 being object st
( e1 in E & e1 Joins v3,v,G1 & ( for e2 being object st e2 Joins v3,v,G1 holds
e1 = e2 ) ) by GLIB_007:def 4;
consider e1 being object such that
A5: ( e1 in E & e1 Joins v2,v,G1 ) and
A6: for e2 being object st e2 Joins v2,v,G1 holds
e1 = e2 by A2, A4;
A7: v2 <> v by A2;

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

suppose x = v ; :: thesis:

then e2 Joins v1,v,G1 by A8, GLIB_000:16;
then e2 = e1 by A1, A6;
then e2 in {e1} by TARSKI:def 1;
hence e2 in (v2 .edgesIn()) \/ {e1} by XBOOLE_0:def 3; :: thesis:

end;

suppose x <> v ; :: thesis:

then A9: e2 DJoins x,v1,G2 by A1, A2, A7, A8, GLIB_007:def 4;
e2 is set by TARSKI:1;
then e2 in v2 .edgesIn() by A1, A9, GLIB_000:57;
hence e2 in (v2 .edgesIn()) \/ {e1} by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

then A10: v1 .edgesIn() c= (v2 .edgesIn()) \/ {e1} by TARSKI:def 3;

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

suppose x = v ; :: thesis:

then e2 Joins v1,v,G1 by A11, GLIB_000:16;
then e2 = e1 by A1, A6;
then e2 in {e1} by TARSKI:def 1;
hence e2 in (v2 .edgesOut()) \/ {e1} by XBOOLE_0:def 3; :: thesis:

end;

suppose x <> v ; :: thesis:

then A12: e2 DJoins v1,x,G2 by A1, A2, A7, A11, GLIB_007:def 4;
e2 is set by TARSKI:1;
then e2 in v2 .edgesOut() by A1, A12, GLIB_000:59;
hence e2 in (v2 .edgesOut()) \/ {e1} by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

then A13: v1 .edgesOut() c= (v2 .edgesOut()) \/ {e1} by TARSKI:def 3;
A14: ( v1 .edgesIn() = v2 .edgesIn() or v1 .edgesOut() = v2 .edgesOut() )

assume A15: ( v1 .edgesIn() <> v2 .edgesIn() & v1 .edgesOut() <> v2 .edgesOut() ) ; :: thesis:
G2 is Subgraph of G1 by GLIB_006:57;
then ( v2 .edgesIn() c= v1 .edgesIn() & v2 .edgesOut() c= v1 .edgesOut() ) by A1, GLIB_000:78;
then ( not v1 .edgesIn() c= v2 .edgesIn() & not v1 .edgesOut() c= v2 .edgesOut() ) by A15, XBOOLE_0:def 10;
then A16: ( (v1 .edgesIn()) \ (v2 .edgesIn()) <> {} & (v1 .edgesOut()) \ (v2 .edgesOut()) <> {} ) by XBOOLE_1:37;
then consider i being object such that
A17: i in (v1 .edgesIn()) \ (v2 .edgesIn()) by XBOOLE_0:def 1;
consider o being object such that
A18: o in (v1 .edgesOut()) \ (v2 .edgesOut()) by A16, XBOOLE_0:def 1;
A19: ( i in v1 .edgesIn() & not i in v2 .edgesIn() & o in v1 .edgesOut() & not o in v2 .edgesOut() ) by A17, A18, XBOOLE_0:def 5;
then ( i in {e1} & o in {e1} ) by A10, A13, XBOOLE_0:def 3;
then A20: ( i = e1 & o = e1 ) by TARSKI:def 1;
then consider j being set such that
A21: e1 DJoins j,v1,G1 by A19, GLIB_000:57;
consider p being set such that
A22: e1 DJoins v1,p,G1 by A19, A20, GLIB_000:59;
( j = v1 & v1 = p ) by A21, A22, GLIB_000:125;
then e1 Joins v1,v1,G1 by A21, GLIB_000:16;
hence contradiction by A1, A5, A7, GLIB_000:15; :: thesis:

end;

{e1} misses the_Edges_of G2 by A3, A5, ZFMISC_1:31, XBOOLE_1:63;
then A23: ( {e1} misses v2 .edgesIn() & {e1} misses v2 .edgesOut() ) by XBOOLE_1:63;
then A24: card ((v2 .edgesOut()) \/ {e1}) = (v2 .outDegree()) +` (card {e1}) by CARD_2:35
.= (v2 .outDegree()) +` 1 by CARD_1:30 ;
A25: card ((v2 .edgesIn()) \/ {e1}) = (v2 .inDegree()) +` (card {e1}) by A23, CARD_2:35
.= (v2 .inDegree()) +` 1 by CARD_1:30 ;
thus v1 .degree() c= (v2 .degree()) +` 1 :: thesis:

per cases by A14;

suppose v1 .edgesIn() = v2 .edgesIn() ; :: thesis:

then A26: v1 .inDegree() = v2 .inDegree() ;
v1 .outDegree() c= (v2 .outDegree()) +` 1 by A13, A24, CARD_1:11;
then v1 .degree() c= (v2 .inDegree()) +` ((v2 .outDegree()) +` 1) by A26, CARD_2:84;
hence v1 .degree() c= (v2 .degree()) +` 1 by CARD_2:19; :: thesis:

end;

suppose v1 .edgesOut() = v2 .edgesOut() ; :: thesis:

then A27: v1 .outDegree() = v2 .outDegree() ;
v1 .inDegree() c= (v2 .inDegree()) +` 1 by A10, A25, CARD_1:11;
then v1 .degree() c= (v2 .outDegree()) +` ((v2 .inDegree()) +` 1) by A27, CARD_2:84;
hence v1 .degree() c= (v2 .degree()) +` 1 by CARD_2:19; :: thesis:

end;

end;

end;

thus ( v1 .inDegree() c= (v2 .inDegree()) +` 1 & v1 .outDegree() c= (v2 .outDegree()) +` 1 ) by A10, A13, A24, A25, CARD_1:11; :: thesis:

end;

suppose not v2 in V ; :: thesis:

then ( v1 .degree() = v2 .degree() & v1 .inDegree() = v2 .inDegree() & v1 .outDegree() = v2 .outDegree() ) by A1, Th62;
hence ( v1 .degree() c= (v2 .degree()) +` 1 & v1 .inDegree() c= (v2 .inDegree()) +` 1 & v1 .outDegree() c= (v2 .outDegree()) +` 1 ) by CARD_2:94; :: 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;
then ( v1 .degree() = v2 .degree() & v1 .inDegree() = v2 .inDegree() & v1 .outDegree() = v2 .outDegree() ) by A1, GLIB_000:96;
hence ( v1 .degree() c= (v2 .degree()) +` 1 & v1 .inDegree() c= (v2 .inDegree()) +` 1 & v1 .outDegree() c= (v2 .outDegree()) +` 1 ) by CARD_2:94; :: thesis:

end;

end;