theorem :: GLIB_012:122

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