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

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

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

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

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

end;

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

end;

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

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

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

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

assume x in v2 .outNeighbors() ; :: thesis: x in (the_Vertices_of G2) \ (v1 .outNeighbors())
then consider e being object such that
A6: e DJoins v2,x,G2 by GLIB_000:70;
e Joins v2,x,G2 by A6, GLIB_000:16;
then A7: x in the_Vertices_of G2 by GLIB_000:13;
then reconsider w = x as Vertex of G1 by Def6;
for e0 being object holds not e0 DJoins v1,w,G1 by A1, A6, Def6;
then not x in v1 .outNeighbors() by GLIB_000:70;
hence x in (the_Vertices_of G2) \ (v1 .outNeighbors()) by A7, XBOOLE_0:def 5; :: thesis: verum

end;

assume x in (the_Vertices_of G2) \ (v1 .outNeighbors()) ; :: thesis: x in v2 .outNeighbors()
then A8: ( x in the_Vertices_of G2 & not x in v1 .outNeighbors() ) by XBOOLE_0:def 5;
then reconsider w = x as Vertex of G1 by Def6;
for e0 being object holds not e0 DJoins v1,w,G1 by A8, GLIB_000:70;
then consider e being object such that
A9: e DJoins v1,w,G2 by Def6;
thus x in v2 .outNeighbors() by A1, A9, GLIB_000:70; :: thesis: verum

end;

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