let G1 be _Graph; :: thesis: ( G1 is self-Dcomplementary implies ( G1 is Dsimple & G1 is connected ) )
set G2 = the DGraphComplement of G1;
assume G1 is self-Dcomplementary ; :: thesis: ( G1 is Dsimple & G1 is connected )
then the DGraphComplement of G1 is G1 -Disomorphic ;
then consider F being PGraphMapping of G1, the DGraphComplement of G1 such that
A3: F is Disomorphism by GLIB_010:def 24;
thus ( G1 is Dsimple & G1 is connected ) by A3, GLIB_010:140, GLIBPRE0:79; :: thesis: verum