theorem :: GLIB_012:123

for G being _Graph holds
( G is self-complementary iff ex H being GraphComplement of G st H is G -isomorphic )