let G1 be _Graph; :: thesis: ( G1 is self-DLcomplementary implies ( not G1 is loopless & not G1 is loopfull & G1 is non-Dmulti & G1 is connected ) )
set G2 = the DLGraphComplement of G1;
assume G1 is self-DLcomplementary ; :: thesis: ( not G1 is loopless & not G1 is loopfull & G1 is non-Dmulti & G1 is connected )
then the DLGraphComplement of G1 is G1 -Disomorphic ;
then consider F being PGraphMapping of G1, the DLGraphComplement of G1 such that
A1: F is Disomorphism by GLIB_010:def 24;
thus ( not G1 is loopless & not G1 is loopfull & G1 is non-Dmulti & G1 is connected ) by A1, GLIB_010:89, GLIB_010:140, GLIBPRE0:79; :: thesis: verum