let G1 be _Graph; :: thesis: for G2 being removeDParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() = v1 .inNeighbors() & v2 .outNeighbors() = v1 .outNeighbors() & v2 .allNeighbors() = v1 .allNeighbors() )
let G2 be removeDParallelEdges of G1; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() = v1 .inNeighbors() & v2 .outNeighbors() = v1 .outNeighbors() & v2 .allNeighbors() = v1 .allNeighbors() )
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() = v1 .inNeighbors() & v2 .outNeighbors() = v1 .outNeighbors() & v2 .allNeighbors() = v1 .allNeighbors() )
let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies ( v2 .inNeighbors() = v1 .inNeighbors() & v2 .outNeighbors() = v1 .outNeighbors() & v2 .allNeighbors() = v1 .allNeighbors() ) )
assume A1: v1 = v2 ; :: thesis: ( v2 .inNeighbors() = v1 .inNeighbors() & v2 .outNeighbors() = v1 .outNeighbors() & v2 .allNeighbors() = v1 .allNeighbors() )
consider E being RepDEdgeSelection of G1 such that
A2: G2 is inducedSubgraph of G1, the_Vertices_of G1,E by GLIB_009:def 8;
the_Edges_of G1 = G1 .edgesBetween (the_Vertices_of G1) by GLIB_000:34;
then ( E c= G1 .edgesBetween (the_Vertices_of G1) & the_Vertices_of G1 c= the_Vertices_of G1 ) ;
then A3: the_Edges_of G2 = E by A2, GLIB_000:def 37;
A4: v2 .inNeighbors() c= v1 .inNeighbors() by A1, GLIB_000:82;

now :: thesis: for x being object st x in v1 .inNeighbors() holds
x in v2 .inNeighbors()

let x be object ; :: thesis: ( x in v1 .inNeighbors() implies x in v2 .inNeighbors() )
assume x in v1 .inNeighbors() ; :: thesis: x in v2 .inNeighbors()
then consider e0 being object such that
A5: e0 DJoins x,v1,G1 by GLIB_000:69;
consider e being object such that
A6: ( e DJoins x,v1,G1 & e in E ) and
for e9 being object st e9 DJoins x,v1,G1 & e9 in E holds
e9 = e by A5, GLIB_009:def 6;
A7: ( x is set & e is set ) by TARSKI:1;
then e DJoins x,v1,G2 by A3, A6, GLIB_000:73;
hence x in v2 .inNeighbors() by A1, A7, GLIB_000:69; :: thesis: verum

end;

then v1 .inNeighbors() c= v2 .inNeighbors() by TARSKI:def 3;
hence A8: v2 .inNeighbors() = v1 .inNeighbors() by A4, XBOOLE_0:def 10; :: thesis: ( v2 .outNeighbors() = v1 .outNeighbors() & v2 .allNeighbors() = v1 .allNeighbors() )
A9: v2 .outNeighbors() c= v1 .outNeighbors() by A1, GLIB_000:82;

now :: thesis: for x being object st x in v1 .outNeighbors() holds
x in v2 .outNeighbors()

let x be object ; :: thesis: ( x in v1 .outNeighbors() implies x in v2 .outNeighbors() )
assume x in v1 .outNeighbors() ; :: thesis: x in v2 .outNeighbors()
then consider e0 being object such that
A10: e0 DJoins v1,x,G1 by GLIB_000:70;
consider e being object such that
A11: ( e DJoins v1,x,G1 & e in E ) and
for e9 being object st e9 DJoins v1,x,G1 & e9 in E holds
e9 = e by A10, GLIB_009:def 6;
A12: ( x is set & e is set ) by TARSKI:1;
then e DJoins v1,x,G2 by A3, A11, GLIB_000:73;
hence x in v2 .outNeighbors() by A1, A12, GLIB_000:70; :: thesis: verum

end;

then v1 .outNeighbors() c= v2 .outNeighbors() by TARSKI:def 3;
hence A13: v2 .outNeighbors() = v1 .outNeighbors() by A9, XBOOLE_0:def 10; :: thesis: v2 .allNeighbors() = v1 .allNeighbors()
thus v2 .allNeighbors() = v1 .allNeighbors() by A8, A13; :: thesis: verum