theorem Th80: :: GLIB_012:80

for G1 being _Graph
for G2 being Dsimple _Graph holds
( G2 is DGraphComplement of G1 iff ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & ( for v, w being Vertex of G1 st v <> w holds
( ex e1 being object st e1 DJoins v,w,G1 iff for e2 being object holds not e2 DJoins v,w,G2 ) ) ) )