let G1 be _Graph; 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; 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; ( ( 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
; ex e being object st e Joins v,w,G2
for e being object holds not e DJoins v,w,G1
then consider e being object such that
A3:
e DJoins v,w,G2
by Def6;
take
e
; e Joins v,w,G2
thus
e Joins v,w,G2
by A3, GLIB_000:16; verum