let G1 be _Graph; for G2 being DLGraphComplement of G1
for e1, e2, v, w being object st e1 DJoins v,w,G1 holds
not e2 DJoins v,w,G2
let G2 be DLGraphComplement of G1; for e1, e2, v, w being object st e1 DJoins v,w,G1 holds
not e2 DJoins v,w,G2
let e1, e2, v, w be object ; ( e1 DJoins v,w,G1 implies not e2 DJoins v,w,G2 )
assume A1:
e1 DJoins v,w,G1
; not e2 DJoins v,w,G2
then
e1 Joins v,w,G1
by GLIB_000:16;
then
( v in the_Vertices_of G1 & w in the_Vertices_of G1 )
by GLIB_000:13;
hence
not e2 DJoins v,w,G2
by A1, Def6; verum