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