let G1 be _Graph; :: thesis: for G2 being reverseEdgeDirections of G1
for G3 being DGraphComplement of G1
for G4 being reverseEdgeDirections of G3 holds G4 is DGraphComplement of G2
let G2 be reverseEdgeDirections of G1; :: thesis: for G3 being DGraphComplement of G1
for G4 being reverseEdgeDirections of G3 holds G4 is DGraphComplement of G2
let G3 be DGraphComplement of G1; :: thesis: for G4 being reverseEdgeDirections of G3 holds G4 is DGraphComplement of G2
let G4 be reverseEdgeDirections of G3; :: thesis: G4 is DGraphComplement of G2
A1: the_Vertices_of G4 = the_Vertices_of G3 by GLIB_007:4
.= the_Vertices_of G1 by Th80
.= the_Vertices_of G2 by GLIB_007:4 ;
the_Edges_of G3 misses the_Edges_of G1 by Th80;
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 st v <> w 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: ( v <> w implies ( ( 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 ) ) )
assume A3: v <> w ; :: 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 ) )
A4: ( 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 A5: e2 DJoins v,w,G2 ; :: thesis: for e4 being object holds not e4 DJoins v,w,G4
e2 in the_Edges_of G2 by A5, GLIB_000:def 14;
then e2 in the_Edges_of G1 by GLIB_007:4;
then A6: e2 DJoins w,v,G1 by A5, GLIB_007:7;
given e4 being object such that A7: e4 DJoins v,w,G4 ; :: thesis: contradiction
e4 in the_Edges_of G4 by A7, GLIB_000:def 14;
then e4 in the_Edges_of G3 by GLIB_007:4;
then e4 DJoins w,v,G3 by A7, GLIB_007:7;
hence contradiction by A6, Th81; :: thesis: verum

end;

assume A8: 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 A9: e3 DJoins w,v,G3 ; :: thesis: contradiction
e3 in the_Edges_of G3 by A9, GLIB_000:def 14;
then e3 DJoins v,w,G4 by A9, GLIB_007:7;
hence contradiction by A8; :: thesis: verum

end;

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

end;

hence G4 is DGraphComplement of G2 by A1, A2, Th80; :: thesis: verum