let G1 be _Graph; :: thesis: for G2 being DSimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() = (v1 .inNeighbors()) \ {v1} & v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} & v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} )
let G2 be DSimpleGraph of G1; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() = (v1 .inNeighbors()) \ {v1} & v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} & v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} )
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() = (v1 .inNeighbors()) \ {v1} & v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} & v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} )
let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies ( v2 .inNeighbors() = (v1 .inNeighbors()) \ {v1} & v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} & v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} ) )
assume A1: v1 = v2 ; :: thesis: ( v2 .inNeighbors() = (v1 .inNeighbors()) \ {v1} & v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} & v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} )
consider G9 being removeDParallelEdges of G1 such that
A2: G2 is removeLoops of G9 by GLIB_009:120;
reconsider v3 = v2 as Vertex of G9 by A2, GLIB_000:53;
thus v2 .inNeighbors() = (v3 .inNeighbors()) \ {v3} by A2, Th69
.= (v1 .inNeighbors()) \ {v1} by A1, Th71 ; :: thesis: ( v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} & v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} )
thus v2 .outNeighbors() = (v3 .outNeighbors()) \ {v3} by A2, Th69
.= (v1 .outNeighbors()) \ {v1} by A1, Th71 ; :: thesis: v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1}
thus v2 .allNeighbors() = (v3 .allNeighbors()) \ {v3} by A2, Th69
.= (v1 .allNeighbors()) \ {v1} by A1, Th71 ; :: thesis: verum