let G1 be _Graph; :: thesis: for G2 being DLGraphComplement of G1
for v, w being Vertex of G1 st ( for e being object holds not e Joins v,w,G1 ) holds
ex e being object st e Joins v,w,G2
let G2 be DLGraphComplement of G1; :: thesis: for v, w being Vertex of G1 st ( for e being object holds not e Joins v,w,G1 ) holds
ex e being object st e Joins v,w,G2
let v, w be Vertex of G1; :: thesis: ( ( for e being object holds not e Joins v,w,G1 ) implies ex e being object st e Joins v,w,G2 )
assume A1: for e being object holds not e Joins v,w,G1 ; :: thesis: ex e being object st e Joins v,w,G2
for e being object holds not e DJoins v,w,G1

proof

given e being object such that A2: e DJoins v,w,G1 ; :: thesis: contradiction
e Joins v,w,G1 by A2, GLIB_000:16;
hence contradiction by A1; :: thesis: verum

end;

then consider e being object such that
A3: e DJoins v,w,G2 by Def6;
take e ; :: thesis: e Joins v,w,G2
thus e Joins v,w,G2 by A3, GLIB_000:16; :: thesis: verum