:: deftheorem Def8 defines DGraphComplement GLIB_012:def 8 :
for G being _Graph
for b₂ being Dsimple _Graph holds
( b₂ is DGraphComplement of G iff ex G9 being DLGraphComplement of G st b₂ is removeLoops of G9 );