theorem :: GLIB_012:120

for G being _Graph holds
( G is self-DLcomplementary iff ex H being DLGraphComplement of G st H is G -Disomorphic )