let G1 be _Graph; :: thesis: ( G1 is self-complementary implies ( G1 is simple & G1 is connected ) )
set G2 = the GraphComplement of G1;
assume G1 is self-complementary ; :: thesis: ( G1 is simple & G1 is connected )
then the GraphComplement of G1 is G1 -isomorphic ;
then consider F being PGraphMapping of G1, the GraphComplement of G1 such that
A4: F is isomorphism by GLIB_010:def 23;
thus ( G1 is simple & G1 is connected ) by A4, GLIB_010:89, GLIB_010:140; :: thesis: verum