theorem Th98: :: GLIB_012:98

for G1 being _Graph
for G2 being simple _Graph holds
( G2 is GraphComplement 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 Joins v,w,G1 iff for e2 being object holds not e2 Joins v,w,G2 ) ) ) )