let G1 be _Graph; :: thesis: for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
v2 .allNeighbors() = (the_Vertices_of G2) \ ((v1 .allNeighbors()) \/ {v2})
let G2 be GraphComplement of G1; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
v2 .allNeighbors() = (the_Vertices_of G2) \ ((v1 .allNeighbors()) \/ {v2})
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds
v2 .allNeighbors() = (the_Vertices_of G2) \ ((v1 .allNeighbors()) \/ {v2})
let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies v2 .allNeighbors() = (the_Vertices_of G2) \ ((v1 .allNeighbors()) \/ {v2}) )
assume A1: v1 = v2 ; :: thesis: v2 .allNeighbors() = (the_Vertices_of G2) \ ((v1 .allNeighbors()) \/ {v2})
consider G9 being LGraphComplement of G1 such that
A2: G2 is removeLoops of G9 by Def9;
reconsider v9 = v1 as Vertex of G9 by Def7;
thus v2 .allNeighbors() = (v9 .allNeighbors()) \ {v2} by A1, A2, GLIBPRE0:63
.= ((the_Vertices_of G9) \ (v1 .allNeighbors())) \ {v2} by Th77
.= (the_Vertices_of G9) \ ((v1 .allNeighbors()) \/ {v2}) by XBOOLE_1:41
.= (the_Vertices_of G2) \ ((v1 .allNeighbors()) \/ {v2}) by A2, GLIB_000:53 ; :: thesis: verum