let G1 be _Graph; :: thesis: for G2 being LGraphComplement 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())
let G2 be LGraphComplement 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())
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())
let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies v2 .allNeighbors() = (the_Vertices_of G2) \ (v1 .allNeighbors()) )
assume A1: v1 = v2 ; :: thesis: v2 .allNeighbors() = (the_Vertices_of G2) \ (v1 .allNeighbors())

now :: thesis: for x being object holds
( ( x in v2 .allNeighbors() implies x in (the_Vertices_of G2) \ (v1 .allNeighbors()) ) & ( x in (the_Vertices_of G2) \ (v1 .allNeighbors()) implies x in v2 .allNeighbors() ) )

let x be object ; :: thesis: ( ( x in v2 .allNeighbors() implies x in (the_Vertices_of G2) \ (v1 .allNeighbors()) ) & ( x in (the_Vertices_of G2) \ (v1 .allNeighbors()) implies x in v2 .allNeighbors() ) )

hereby :: thesis: ( x in (the_Vertices_of G2) \ (v1 .allNeighbors()) implies x in v2 .allNeighbors() )

assume x in v2 .allNeighbors() ; :: thesis: x in (the_Vertices_of G2) \ (v1 .allNeighbors())
then consider e being object such that
A2: e Joins v2,x,G2 by GLIB_000:71;
A3: x in the_Vertices_of G2 by A2, GLIB_000:13;
then reconsider w = x as Vertex of G1 by Def7;
for e0 being object holds not e0 Joins v1,w,G1 by A1, A2, Def7;
then not x in v1 .allNeighbors() by GLIB_000:71;
hence x in (the_Vertices_of G2) \ (v1 .allNeighbors()) by A3, XBOOLE_0:def 5; :: thesis: verum

end;

assume x in (the_Vertices_of G2) \ (v1 .allNeighbors()) ; :: thesis: x in v2 .allNeighbors()
then A4: ( x in the_Vertices_of G2 & not x in v1 .allNeighbors() ) by XBOOLE_0:def 5;
then reconsider w = x as Vertex of G1 by Def7;
for e0 being object holds not e0 Joins v1,w,G1 by A4, GLIB_000:71;
then consider e being object such that
A5: e Joins v1,w,G2 by Def7;
thus x in v2 .allNeighbors() by A1, A5, GLIB_000:71; :: thesis: verum

end;

hence v2 .allNeighbors() = (the_Vertices_of G2) \ (v1 .allNeighbors()) by TARSKI:2; :: thesis: verum