let G2 be _Graph; :: thesis: for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w
for v1 being Vertex of G1 st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & v1 = v holds
( v1 .edgesIn() = v .edgesIn() & v1 .inDegree() = v .inDegree() & v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 )
let v be Vertex of G2; :: thesis: for e, w being object
for G1 being addAdjVertex of G2,v,e,w
for v1 being Vertex of G1 st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & v1 = v holds
( v1 .edgesIn() = v .edgesIn() & v1 .inDegree() = v .inDegree() & v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 )
let e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w
for v1 being Vertex of G1 st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & v1 = v holds
( v1 .edgesIn() = v .edgesIn() & v1 .inDegree() = v .inDegree() & v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 )
let G1 be addAdjVertex of G2,v,e,w; :: thesis: for v1 being Vertex of G1 st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & v1 = v holds
( v1 .edgesIn() = v .edgesIn() & v1 .inDegree() = v .inDegree() & v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 )
let v1 be Vertex of G1; :: thesis: ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 & v1 = v implies ( v1 .edgesIn() = v .edgesIn() & v1 .inDegree() = v .inDegree() & v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 ) )
assume A1: ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 & v1 = v ) ; :: thesis: ( v1 .edgesIn() = v .edgesIn() & v1 .inDegree() = v .inDegree() & v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 )
then consider G3 being addVertex of G2,w such that
A2: G1 is addEdge of G3,v,e,w by GLIB_006:125;
reconsider v3 = v as Vertex of G3 by GLIB_006:68;
A3: ( v3 .edgesIn() = v .edgesIn() & v3 .inDegree() = v .inDegree() & v3 .edgesOut() = v .edgesOut() & v3 .outDegree() = v .outDegree() & v3 .edgesInOut() = v .edgesInOut() & v3 .degree() = v .degree() ) by GLIBPRE0:45;
A4: the_Edges_of G3 = the_Edges_of G2 by GLIB_006:def 10;
w in {w} by TARSKI:def 1;
then A5: w is Vertex of G3 by GLIB_006:86;
v <> w by A1;
hence ( v1 .edgesIn() = v .edgesIn() & v1 .inDegree() = v .inDegree() & v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 ) by A1, A2, A3, A4, A5, GLIBPRE0:47; :: thesis: verum