theorem :: GLIB_012:63

for G1 being _Graph
for G2 being non-multi _Graph holds
( G2 is LGraphComplement of G1 iff ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & ( for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 holds
( v1,w1 are_adjacent iff not v2,w2 are_adjacent ) ) ) )