:: deftheorem Def7 defines LGraphComplement GLIB_012:def 7 :
for G being _Graph
for b₂ being non-multi _Graph holds
( b₂ is LGraphComplement of G iff ( the_Vertices_of b₂ = the_Vertices_of G & the_Edges_of b₂ misses the_Edges_of G & ( for v, w being Vertex of G holds
( ex e1 being object st e1 Joins v,w,G iff for e2 being object holds not e2 Joins v,w,b₂ ) ) ) );