let G1 be _Graph; for G2 being DLGraphComplement of G1 holds
( ( G1 is _trivial implies G2 is _trivial ) & ( G2 is _trivial implies G1 is _trivial ) & ( G1 is loopfull implies G2 is loopless ) & ( G2 is loopless implies G1 is loopfull ) & ( G1 is loopless implies G2 is loopfull ) & ( G2 is loopfull implies G1 is loopless ) )
let G2 be DLGraphComplement of G1; ( ( G1 is _trivial implies G2 is _trivial ) & ( G2 is _trivial implies G1 is _trivial ) & ( G1 is loopfull implies G2 is loopless ) & ( G2 is loopless implies G1 is loopfull ) & ( G1 is loopless implies G2 is loopfull ) & ( G2 is loopfull implies G1 is loopless ) )
hereby ( ( G2 is loopless implies G1 is loopfull ) & ( G1 is loopless implies G2 is loopfull ) & ( G2 is loopfull implies G1 is loopless ) )
assume A1:
G1 is
loopfull
;
G2 is loopless now for v, e2 being object holds not e2 DJoins v,v,G2let v be
object ;
for e2 being object holds not e2 DJoins v,v,G2given e2 being
object such that A2:
e2 DJoins v,
v,
G2
;
contradiction
e2 Joins v,
v,
G2
by A2, GLIB_000:16;
then
v in the_Vertices_of G2
by GLIB_000:13;
then
v in the_Vertices_of G1
by Def6;
then consider e1 being
object such that A3:
e1 DJoins v,
v,
G1
by A1, Th1;
thus
contradiction
by A2, A3, Th46;
verum end; hence
G2 is
loopless
by GLIB_009:17;
verum
end;
hereby verum
assume A7:
G2 is
loopfull
;
G1 is loopless now for v, e1 being object holds not e1 DJoins v,v,G1let v be
object ;
for e1 being object holds not e1 DJoins v,v,G1given e1 being
object such that A8:
e1 DJoins v,
v,
G1
;
contradiction
e1 Joins v,
v,
G1
by A8, GLIB_000:16;
then
v in the_Vertices_of G1
by GLIB_000:13;
then
v in the_Vertices_of G2
by Def6;
then consider e2 being
object such that A9:
e2 DJoins v,
v,
G2
by A7, Th1;
thus
contradiction
by A8, A9, Th46;
verum end; hence
G1 is
loopless
by GLIB_009:17;
verum
end;