let G1 be _Graph; :: thesis: for G2 being reverseEdgeDirections of G1
for G3 being DLGraphComplement of G1
for G4 being reverseEdgeDirections of G3 holds G4 is DLGraphComplement of G2
let G2 be reverseEdgeDirections of G1; :: thesis: for G3 being DLGraphComplement of G1
for G4 being reverseEdgeDirections of G3 holds G4 is DLGraphComplement of G2
let G3 be DLGraphComplement of G1; :: thesis: for G4 being reverseEdgeDirections of G3 holds G4 is DLGraphComplement of G2
let G4 be reverseEdgeDirections of G3; :: thesis: G4 is DLGraphComplement of G2
A1: the_Vertices_of G4 = the_Vertices_of G3 by GLIB_007:4
.= the_Vertices_of G1 by Def6
.= the_Vertices_of G2 by GLIB_007:4 ;
the_Edges_of G3 misses the_Edges_of G1 by Def6;
then the_Edges_of G4 misses the_Edges_of G1 by GLIB_007:4;
then A2: the_Edges_of G4 misses the_Edges_of G2 by GLIB_007:4;

now :: thesis: for v, w being Vertex of G2 holds
( ( ex e2 being object st e2 DJoins v,w,G2 implies for e4 being object holds not e4 DJoins v,w,G4 ) & ( ( for e4 being object holds not e4 DJoins v,w,G4 ) implies ex e1 being object st e1 DJoins v,w,G2 ) )

let v, w be Vertex of G2; :: thesis: ( ( ex e2 being object st e2 DJoins v,w,G2 implies for e4 being object holds not e4 DJoins v,w,G4 ) & ( ( for e4 being object holds not e4 DJoins v,w,G4 ) implies ex e1 being object st e1 DJoins v,w,G2 ) )
A3: ( v is Vertex of G1 & w is Vertex of G1 ) by GLIB_007:4;

hereby :: thesis: ( ( for e4 being object holds not e4 DJoins v,w,G4 ) implies ex e1 being object st e1 DJoins v,w,G2 )

given e2 being object such that A4: e2 DJoins v,w,G2 ; :: thesis: for e4 being object holds not e4 DJoins v,w,G4
e2 in the_Edges_of G2 by A4, GLIB_000:def 14;
then e2 in the_Edges_of G1 by GLIB_007:4;
then A5: e2 DJoins w,v,G1 by A4, GLIB_007:7;
given e4 being object such that A6: e4 DJoins v,w,G4 ; :: thesis: contradiction
e4 in the_Edges_of G4 by A6, GLIB_000:def 14;
then e4 in the_Edges_of G3 by GLIB_007:4;
then e4 DJoins w,v,G3 by A6, GLIB_007:7;
hence contradiction by A5, Th46; :: thesis: verum

end;

assume A7: for e4 being object holds not e4 DJoins v,w,G4 ; :: thesis: ex e1 being object st e1 DJoins v,w,G2
for e3 being object holds not e3 DJoins w,v,G3

proof

given e3 being object such that A8: e3 DJoins w,v,G3 ; :: thesis: contradiction
e3 in the_Edges_of G3 by A8, GLIB_000:def 14;
then e3 DJoins v,w,G4 by A8, GLIB_007:7;
hence contradiction by A7; :: thesis: verum

end;

then consider e1 being object such that
A9: e1 DJoins w,v,G1 by A3, Def6;
take e1 = e1; :: thesis: e1 DJoins v,w,G2
e1 in the_Edges_of G1 by A9, GLIB_000:def 14;
hence e1 DJoins v,w,G2 by A9, GLIB_007:7; :: thesis: verum

end;

hence G4 is DLGraphComplement of G2 by A1, A2, Def6; :: thesis: verum