let G be _Graph; :: thesis: ( G is self-Dcomplementary & G is self-complementary implies ( G is _trivial & G is edgeless ) )
assume A1: ( G is self-Dcomplementary & G is self-complementary ) ; :: thesis: ( G is _trivial & G is edgeless )
set H1 = the DGraphComplement of G;
set H2 = the GraphComplement of G;
the DGraphComplement of G is G -Disomorphic by A1;
then consider F1 being PGraphMapping of G, the DGraphComplement of G such that
A2: F1 is Disomorphism by GLIB_010:def 24;
the GraphComplement of G is G -isomorphic by A1;
then consider F2 being PGraphMapping of G, the GraphComplement of G such that
A3: F2 is isomorphism by GLIB_010:def 23;

now :: thesis: for v1, v2 being Vertex of G st v1 <> v2 holds
v1,v2 are_adjacent

let v1, v2 be Vertex of G; :: thesis: ( v1 <> v2 implies v1,v2 are_adjacent )
assume A4: v1 <> v2 ; :: thesis: v1,v2 are_adjacent
assume A5: not v1,v2 are_adjacent ; :: thesis: contradiction
for e being object holds not e DJoins v1,v2,G

proof

given e being object such that A6: e DJoins v1,v2,G ; :: thesis: contradiction
e Joins v1,v2,G by A6, GLIB_000:16;
hence contradiction by A5, CHORD:def 3; :: thesis: verum

end;

then consider e1 being object such that
A7: e1 DJoins v1,v2, the DGraphComplement of G by A4, Th80;
for e being object holds not e DJoins v2,v1,G

proof

given e being object such that A8: e DJoins v2,v1,G ; :: thesis: contradiction
e Joins v1,v2,G by A8, GLIB_000:16;
hence contradiction by A5, CHORD:def 3; :: thesis: verum

end;

then consider e2 being object such that
A9: e2 DJoins v2,v1, the DGraphComplement of G by A4, Th80;
A10: ( e1 Joins v1,v2, the DGraphComplement of G & e2 Joins v1,v2, the DGraphComplement of G ) by A7, A9, GLIB_000:16;
the DGraphComplement of G is non-multi by A1, A2, GLIB_010:89;
then e1 = e2 by A10, GLIB_000:def 20;
hence contradiction by A4, A7, A9, GLIB_000:125; :: thesis: verum

end;

then G is complete by CHORD:def 6;
hence ( G is _trivial & G is edgeless ) by A3, GLIB_010:89; :: thesis: verum