let G1 be _Graph; :: thesis: 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; :: thesis: ( ( 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 :: thesis: ( ( 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 ) )

assume G1 is _trivial ; :: thesis: G2 is _trivial
then 1 = G1 .order() by GLIB_000:26
.= G2 .order() by Th55 ;
hence G2 is _trivial by GLIB_000:26; :: thesis: verum

end;

hereby :: thesis: ( ( 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 ) )

assume G2 is _trivial ; :: thesis: G1 is _trivial
then 1 = G2 .order() by GLIB_000:26
.= G1 .order() by Th55 ;
hence G1 is _trivial by GLIB_000:26; :: thesis: verum

end;

hereby :: thesis: ( ( 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 ; :: thesis: G2 is loopless

now :: thesis: for v, e2 being object holds not e2 DJoins v,v,G2

let v be object ; :: thesis: for e2 being object holds not e2 DJoins v,v,G2
given e2 being object such that A2: e2 DJoins v,v,G2 ; :: thesis: 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; :: thesis: verum

end;

hence G2 is loopless by GLIB_000:136; :: thesis: verum

end;

hereby :: thesis: ( G1 is loopless iff G2 is loopfull )

assume A4: G2 is loopless ; :: thesis: G1 is loopfull

now :: thesis: for v being Vertex of G1 ex e1 being object st e1 DJoins v,v,G1

let v be Vertex of G1; :: thesis: ex e1 being object st e1 DJoins v,v,G1
assume for e1 being object holds not e1 DJoins v,v,G1 ; :: thesis: contradiction
then ex e2 being object st e2 DJoins v,v,G2 by Def6;
hence contradiction by A4, GLIB_000:136; :: thesis: verum

end;

hence G1 is loopfull by Th1; :: thesis: verum

end;

hereby :: thesis: ( G2 is loopfull implies G1 is loopless )

assume A5: G1 is loopless ; :: thesis: G2 is loopfull

now :: thesis: for v being Vertex of G2 ex e2 being object st e2 DJoins v,v,G2

let v be Vertex of G2; :: thesis: ex e2 being object st e2 DJoins v,v,G2
A6: v is Vertex of G1 by Def6;
assume for e2 being object holds not e2 DJoins v,v,G2 ; :: thesis: contradiction
then ex e1 being object st e1 DJoins v,v,G1 by A6, Def6;
hence contradiction by A5, GLIB_000:136; :: thesis: verum

end;

hence G2 is loopfull by Th1; :: thesis: verum

end;

hereby :: thesis: verum

assume A7: G2 is loopfull ; :: thesis: G1 is loopless

now :: thesis: for v, e1 being object holds not e1 DJoins v,v,G1

let v be object ; :: thesis: for e1 being object holds not e1 DJoins v,v,G1
given e1 being object such that A8: e1 DJoins v,v,G1 ; :: thesis: 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; :: thesis: verum

end;

hence G1 is loopless by GLIB_000:136; :: thesis: verum

end;