let G2 be _Graph; :: thesis: for v, e, w being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for v1 being Vertex of G1 st v1 <> v & v1 <> w & v1 = v2 holds
( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
let v, e, w be object ; :: thesis: for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for v1 being Vertex of G1 st v1 <> v & v1 <> w & v1 = v2 holds
( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
let v2 be Vertex of G2; :: thesis: for G1 being addAdjVertex of G2,v,e,w
for v1 being Vertex of G1 st v1 <> v & v1 <> w & v1 = v2 holds
( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
let G1 be addAdjVertex of G2,v,e,w; :: thesis: for v1 being Vertex of G1 st v1 <> v & v1 <> w & v1 = v2 holds
( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
let v1 be Vertex of G1; :: thesis: ( v1 <> v & v1 <> w & v1 = v2 implies ( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() ) )
assume A1: ( v1 <> v & v1 <> w & v1 = v2 ) ; :: thesis: ( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )

per cases ( ( v in the_Vertices_of G2 & not w in the_Vertices_of G2 & not e in the_Edges_of G2 ) or ( not v in the_Vertices_of G2 & w in the_Vertices_of G2 & not e in the_Edges_of G2 ) or ( not ( v in the_Vertices_of G2 & not w in the_Vertices_of G2 & not e in the_Edges_of G2 ) & not ( not v in the_Vertices_of G2 & w in the_Vertices_of G2 & not e in the_Edges_of G2 ) ) ) ;

suppose ( v in the_Vertices_of G2 & not w in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis: ( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )

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 = v2 as Vertex of G3 by GLIB_006:68;
( v3 .edgesIn() = v2 .edgesIn() & v3 .inDegree() = v2 .inDegree() & v3 .edgesOut() = v2 .edgesOut() & v3 .outDegree() = v2 .outDegree() & v3 .edgesInOut() = v2 .edgesInOut() & v3 .degree() = v2 .degree() ) by GLIBPRE0:45;
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, A2, GLIBPRE0:46; :: thesis: verum

end;

suppose ( not v in the_Vertices_of G2 & w in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis: ( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )

then consider G3 being addVertex of G2,v such that
A3: G1 is addEdge of G3,v,e,w by GLIB_006:126;
reconsider v3 = v2 as Vertex of G3 by GLIB_006:68;
( v3 .edgesIn() = v2 .edgesIn() & v3 .inDegree() = v2 .inDegree() & v3 .edgesOut() = v2 .edgesOut() & v3 .outDegree() = v2 .outDegree() & v3 .edgesInOut() = v2 .edgesInOut() & v3 .degree() = v2 .degree() ) by GLIBPRE0:45;
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, A3, GLIBPRE0:46; :: thesis: verum

end;

suppose ( not ( v in the_Vertices_of G2 & not w in the_Vertices_of G2 & not e in the_Edges_of G2 ) & not ( not v in the_Vertices_of G2 & w in the_Vertices_of G2 & not e in the_Edges_of G2 ) ) ; :: thesis: ( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )

then G1 == G2 by GLIB_006:def 12;
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: verum

end;

end;