let G be _Graph; :: thesis: ( G is self-DLcomplementary implies ( not G is _trivial & not G is self-Lcomplementary & not G is self-Dcomplementary & not G is self-complementary ) )
assume A11: G is self-DLcomplementary ; :: thesis: ( not G is _trivial & not G is self-Lcomplementary & not G is self-Dcomplementary & not G is self-complementary )
hence A12: not G is _trivial ; :: thesis: ( not G is self-Lcomplementary & not G is self-Dcomplementary & not G is self-complementary )
thus not G is self-Lcomplementary :: thesis: ( not G is self-Dcomplementary & not G is self-complementary )

proof

assume A13: G is self-Lcomplementary ; :: thesis: contradiction
set H1 = the DLGraphComplement of G;
set H2 = the LGraphComplement of G;
the DLGraphComplement of G is G -Disomorphic by A11;
then consider F1 being PGraphMapping of G, the DLGraphComplement of G such that
A14: F1 is Disomorphism by GLIB_010:def 24;
the LGraphComplement of G is G -isomorphic by A13;
then consider F2 being PGraphMapping of G, the LGraphComplement of G such that
A15: 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 A16: v1 <> v2 ; :: thesis: v1,v2 are_adjacent
assume A17: 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 A18: e DJoins v1,v2,G ; :: thesis: contradiction
e Joins v1,v2,G by A18, GLIB_000:16;
hence contradiction by A17, CHORD:def 3; :: thesis: verum

end;

then consider e1 being object such that
A19: e1 DJoins v1,v2, the DLGraphComplement of G by Def6;
for e being object holds not e DJoins v2,v1,G

proof

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

end;

then consider e2 being object such that
A21: e2 DJoins v2,v1, the DLGraphComplement of G by Def6;
A22: ( e1 Joins v1,v2, the DLGraphComplement of G & e2 Joins v1,v2, the DLGraphComplement of G ) by A19, A21, GLIB_000:16;
the DLGraphComplement of G is non-multi by A13, A14, GLIB_010:89;
then e1 = e2 by A22, GLIB_000:def 20;
hence contradiction by A16, A19, A21, GLIB_000:125; :: thesis: verum

end;

then A23: G is complete by CHORD:def 6;
then A24: the_Edges_of the LGraphComplement of G = the LGraphComplement of G .loops() by Th75;
consider v1, v2 being Vertex of G such that
A25: v1 <> v2 by A12, GLIB_000:21;
consider e being object such that
A26: e Joins v1,v2,G by A23, A25, CHORD:def 6, CHORD:def 3;
( dom (F2 _E) = the_Edges_of G & dom (F2 _V) = the_Vertices_of G ) by A15, GLIB_010:def 11;
then A27: ( e in dom (F2 _E) & v1 in dom (F2 _V) & v2 in dom (F2 _V) ) by A26, GLIB_000:def 13;
then A28: (F2 _E) . e Joins (F2 _V) . v1,(F2 _V) . v2, the LGraphComplement of G by A26, GLIB_010:4;
(F2 _V) . v1 <> (F2 _V) . v2 by A15, A25, A27, FUNCT_1:def 4;
then not (F2 _E) . e in the LGraphComplement of G .loops() by A28, GLIB_009:46;
hence contradiction by A24, A28, GLIB_000:def 13; :: thesis: verum

end;

thus ( not G is self-Dcomplementary & not G is self-complementary ) by A11; :: thesis: verum