let G1 be _Graph; :: thesis: for G2 being DGraphComplement 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 DGraphComplement of G1; :: thesis: 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 ; :: thesis: ( e1 DJoins v,w,G1 implies not e2 DJoins v,w,G2 )
assume A1: e1 DJoins v,w,G1 ; :: thesis: not e2 DJoins v,w,G2

per cases ( v <> w or v = w ) ;

suppose A2: v <> w ; :: thesis: not e2 DJoins v,w,G2

e1 Joins v,w,G1 by A1, GLIB_000:16;
then ( v is Vertex of G1 & w is Vertex of G1 ) by GLIB_000:13;
hence not e2 DJoins v,w,G2 by A1, A2, Th80; :: thesis: verum

end;

suppose v = w ; :: thesis: not e2 DJoins v,w,G2

hence not e2 DJoins v,w,G2 by GLIB_000:136; :: thesis: verum

end;

end;