let G2 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st 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 be set ; :: thesis: for G1 being addVertices of G2,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st 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 addVertices of G2,V; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st 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: for v2 being Vertex of G2 st 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: ( 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 = 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() )
A2: G2 is Subgraph of G1 by GLIB_006:57;
then A3: v2 .edgesIn() c= v1 .edgesIn() by A1, GLIB_000:78;

now :: thesis: for e being object st e in v1 .edgesIn() holds
e in v2 .edgesIn()

let e be object ; :: thesis: ( e in v1 .edgesIn() implies e in v2 .edgesIn() )
assume e in v1 .edgesIn() ; :: thesis: e in v2 .edgesIn()
then consider x being set such that
A4: e DJoins x,v1,G1 by GLIB_000:57;
( e DJoins x,v2,G2 & e is set ) by A1, A4, GLIB_006:85, TARSKI:1;
hence e in v2 .edgesIn() by GLIB_000:57; :: thesis: verum

end;

then v1 .edgesIn() c= v2 .edgesIn() by TARSKI:def 3;
hence A5: v1 .edgesIn() = v2 .edgesIn() by A3, XBOOLE_0:def 10; :: thesis: ( v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
hence A6: v1 .inDegree() = v2 .inDegree() ; :: thesis: ( v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
A7: v2 .edgesOut() c= v1 .edgesOut() by A1, A2, GLIB_000:78;

now :: thesis: for e being object st e in v1 .edgesOut() holds
e in v2 .edgesOut()

let e be object ; :: thesis: ( e in v1 .edgesOut() implies e in v2 .edgesOut() )
assume e in v1 .edgesOut() ; :: thesis: e in v2 .edgesOut()
then consider x being set such that
A8: e DJoins v1,x,G1 by GLIB_000:59;
( e DJoins v2,x,G2 & e is set ) by A1, A8, GLIB_006:85, TARSKI:1;
hence e in v2 .edgesOut() by GLIB_000:59; :: thesis: verum

end;

then v1 .edgesOut() c= v2 .edgesOut() by TARSKI:def 3;
hence A9: v1 .edgesOut() = v2 .edgesOut() by A7, XBOOLE_0:def 10; :: thesis: ( v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
hence A10: v1 .outDegree() = v2 .outDegree() ; :: thesis: ( v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
thus v1 .edgesInOut() = v2 .edgesInOut() by A5, A9; :: thesis: v1 .degree() = v2 .degree()
thus v1 .degree() = v2 .degree() by A6, A10; :: thesis: verum