:: deftheorem Def9 defines GraphComplement GLIB_012:def 9 :
for G being _Graph
for b₂ being simple _Graph holds
( b₂ is GraphComplement of G iff ex G9 being LGraphComplement of G st b₂ is removeLoops of G9 );