let G1, G2, G3 be _Graph; :: thesis: for G4 being DLGraphComplement of G1 st G1 == G2 & G3 == G4 holds
G3 is DLGraphComplement of G2
let G4 be DLGraphComplement of G1; :: thesis: ( G1 == G2 & G3 == G4 implies G3 is DLGraphComplement of G2 )
assume A1: ( G1 == G2 & G3 == G4 ) ; :: thesis: G3 is DLGraphComplement of G2
then ( the_Vertices_of G4 = the_Vertices_of G3 & the_Edges_of G4 = the_Edges_of G3 ) by GLIB_000:def 34;
then ( the_Vertices_of G1 = the_Vertices_of G3 & the_Edges_of G3 misses the_Edges_of G1 ) by Def6;
then A2: ( the_Vertices_of G3 = the_Vertices_of G2 & the_Edges_of G3 misses the_Edges_of G2 ) by A1, GLIB_000:def 34;
A3: G3 is non-Dmulti by A1, GLIB_000:89;

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

let v, w be Vertex of G2; :: thesis: ( ( ex e1 being object st e1 DJoins v,w,G2 implies for e2 being object holds not e2 DJoins v,w,G3 ) & ( ( for e2 being object holds not e2 DJoins v,w,G3 ) implies ex e1 being object st e1 DJoins v,w,G2 ) )
A4: ( v is Vertex of G1 & w is Vertex of G1 ) by A1, GLIB_000:def 34;

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

given e1 being object such that A5: e1 DJoins v,w,G2 ; :: thesis: for e2 being object holds not e2 DJoins v,w,G3
A6: e1 DJoins v,w,G1 by A1, A5, GLIB_000:88;
thus for e2 being object holds not e2 DJoins v,w,G3 :: thesis: verum

proof

given e2 being object such that A7: e2 DJoins v,w,G3 ; :: thesis: contradiction
e2 DJoins v,w,G4 by A1, A7, GLIB_000:88;
hence contradiction by A4, A6, Def6; :: thesis: verum

end;

end;

assume A8: for e2 being object holds not e2 DJoins v,w,G3 ; :: thesis: ex e1 being object st e1 DJoins v,w,G2
for e2 being object holds not e2 DJoins v,w,G4

proof

given e2 being object such that A9: e2 DJoins v,w,G4 ; :: thesis: contradiction
e2 DJoins v,w,G3 by A1, A9, GLIB_000:88;
hence contradiction by A8; :: thesis: verum

end;

then consider e1 being object such that
A10: e1 DJoins v,w,G1 by A4, Def6;
take e1 = e1; :: thesis: e1 DJoins v,w,G2
thus e1 DJoins v,w,G2 by A1, A10, GLIB_000:88; :: thesis: verum

end;

hence G3 is DLGraphComplement of G2 by A2, A3, Def6; :: thesis: verum