let G1 be _Graph; :: thesis: ( G1 is self-Lcomplementary implies ( not G1 is loopless & not G1 is loopfull & G1 is non-multi & G1 is connected ) )
set G2 = the LGraphComplement of G1;
assume G1 is self-Lcomplementary ; :: thesis: ( not G1 is loopless & not G1 is loopfull & G1 is non-multi & G1 is connected )
then the LGraphComplement of G1 is G1 -isomorphic ;
then consider F being PGraphMapping of G1, the LGraphComplement of G1 such that
A2: F is isomorphism by GLIB_010:def 23;
thus ( not G1 is loopless & not G1 is loopfull & G1 is non-multi & G1 is connected ) by A2, GLIB_010:89, GLIB_010:140; :: thesis: verum