let G1 be _Graph; :: thesis: for G2 being DGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() = (the_Vertices_of G2) \ ((v1 .inNeighbors()) \/ {v2}) & v2 .outNeighbors() = (the_Vertices_of G2) \ ((v1 .outNeighbors()) \/ {v2}) )
let G2 be DGraphComplement of G1; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() = (the_Vertices_of G2) \ ((v1 .inNeighbors()) \/ {v2}) & v2 .outNeighbors() = (the_Vertices_of G2) \ ((v1 .outNeighbors()) \/ {v2}) )
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() = (the_Vertices_of G2) \ ((v1 .inNeighbors()) \/ {v2}) & v2 .outNeighbors() = (the_Vertices_of G2) \ ((v1 .outNeighbors()) \/ {v2}) )
let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies ( v2 .inNeighbors() = (the_Vertices_of G2) \ ((v1 .inNeighbors()) \/ {v2}) & v2 .outNeighbors() = (the_Vertices_of G2) \ ((v1 .outNeighbors()) \/ {v2}) ) )
assume A1: v1 = v2 ; :: thesis: ( v2 .inNeighbors() = (the_Vertices_of G2) \ ((v1 .inNeighbors()) \/ {v2}) & v2 .outNeighbors() = (the_Vertices_of G2) \ ((v1 .outNeighbors()) \/ {v2}) )
consider G9 being DLGraphComplement of G1 such that
A2: G2 is removeLoops of G9 by Def8;
reconsider v9 = v1 as Vertex of G9 by Def6;
thus v2 .inNeighbors() = (v9 .inNeighbors()) \ {v2} by A1, A2, GLIBPRE0:63
.= ((the_Vertices_of G9) \ (v1 .inNeighbors())) \ {v2} by Th60
.= (the_Vertices_of G9) \ ((v1 .inNeighbors()) \/ {v2}) by XBOOLE_1:41
.= (the_Vertices_of G2) \ ((v1 .inNeighbors()) \/ {v2}) by A2, GLIB_000:53 ; :: thesis: v2 .outNeighbors() = (the_Vertices_of G2) \ ((v1 .outNeighbors()) \/ {v2})
thus v2 .outNeighbors() = (v9 .outNeighbors()) \ {v2} by A1, A2, GLIBPRE0:63
.= ((the_Vertices_of G9) \ (v1 .outNeighbors())) \ {v2} by Th60
.= (the_Vertices_of G9) \ ((v1 .outNeighbors()) \/ {v2}) by XBOOLE_1:41
.= (the_Vertices_of G2) \ ((v1 .outNeighbors()) \/ {v2}) by A2, GLIB_000:53 ; :: thesis: verum