let G1 be _Graph; :: thesis: for G2 being GraphComplement of G1 holds
( ( G1 is complete implies G2 is edgeless ) & ( G2 is edgeless implies G1 is complete ) & ( the_Edges_of G1 = G1 .loops() implies G2 is complete ) & ( G2 is complete implies the_Edges_of G1 = G1 .loops() ) )
let G2 be GraphComplement of G1; :: thesis: ( ( G1 is complete implies G2 is edgeless ) & ( G2 is edgeless implies G1 is complete ) & ( the_Edges_of G1 = G1 .loops() implies G2 is complete ) & ( G2 is complete implies the_Edges_of G1 = G1 .loops() ) )

hereby :: thesis: ( ( G2 is edgeless implies G1 is complete ) & ( the_Edges_of G1 = G1 .loops() implies G2 is complete ) & ( G2 is complete implies the_Edges_of G1 = G1 .loops() ) )

assume A1: G1 is complete ; :: thesis: G2 is edgeless

now :: thesis: for v2, w2 being Vertex of G2 st v2 <> w2 holds
not v2,w2 are_adjacent

let v2, w2 be Vertex of G2; :: thesis: ( v2 <> w2 implies not v2,w2 are_adjacent )
assume A2: v2 <> w2 ; :: thesis: not v2,w2 are_adjacent
reconsider v1 = v2, w1 = w2 as Vertex of G1 by Th99;
v1,w1 are_adjacent by A1, A2, CHORD:def 6;
hence not v2,w2 are_adjacent by A2, Th99; :: thesis: verum

end;

hence G2 is edgeless by GLIBPRE0:60; :: thesis: verum

end;

hereby :: thesis: ( the_Edges_of G1 = G1 .loops() iff G2 is complete )

assume A3: G2 is edgeless ; :: thesis: G1 is complete

now :: thesis: for v1, w1 being Vertex of G1 st v1 <> w1 holds
v1,w1 are_adjacent

let v1, w1 be Vertex of G1; :: thesis: ( v1 <> w1 implies v1,w1 are_adjacent )
assume A4: v1 <> w1 ; :: thesis: v1,w1 are_adjacent
reconsider v2 = v1, w2 = w1 as Vertex of G2 by Th99;
not v2,w2 are_adjacent by A3, A4, GLIBPRE0:60;
hence v1,w1 are_adjacent by A4, Th99; :: thesis: verum

end;

hence G1 is complete by CHORD:def 6; :: thesis: verum

end;

hereby :: thesis: ( G2 is complete implies the_Edges_of G1 = G1 .loops() )

assume A5: the_Edges_of G1 = G1 .loops() ; :: thesis: G2 is complete

now :: thesis: for v2, w2 being Vertex of G2 st v2 <> w2 holds
v2,w2 are_adjacent

let v2, w2 be Vertex of G2; :: thesis: ( v2 <> w2 implies v2,w2 are_adjacent )
assume A6: v2 <> w2 ; :: thesis: v2,w2 are_adjacent
reconsider v1 = v2, w1 = w2 as Vertex of G1 by Th98;
for e1 being object holds not e1 Joins v1,w1,G1

proof

given e1 being object such that A7: e1 Joins v1,w1,G1 ; :: thesis: contradiction
e1 in G1 .loops() by A5, A7, GLIB_000:def 13;
then consider v9 being object such that
A8: e1 Joins v9,v9,G1 by GLIB_009:def 2;
( v1 = v9 & w1 = v9 ) by A7, A8, GLIB_000:15;
hence contradiction by A6; :: thesis: verum

end;

then ex e2 being object st e2 Joins v1,w1,G2 by A6, Th98;
hence v2,w2 are_adjacent by CHORD:def 3; :: thesis: verum

end;

hence G2 is complete by CHORD:def 6; :: thesis: verum

end;

hereby :: thesis: verum

assume A9: G2 is complete ; :: thesis: the_Edges_of G1 = G1 .loops()

now :: thesis: for e being object st e in the_Edges_of G1 holds
e in G1 .loops()

let e be object ; :: thesis: ( e in the_Edges_of G1 implies e in G1 .loops() )
assume A10: e in the_Edges_of G1 ; :: thesis: e in G1 .loops()
then reconsider v1 = (the_Source_of G1) . e, w1 = (the_Target_of G1) . e as Vertex of G1 by FUNCT_2:5;
A11: e Joins v1,w1,G1 by A10, GLIB_000:def 13;
then A12: v1,w1 are_adjacent by CHORD:def 3;
reconsider v2 = v1, w2 = w1 as Vertex of G2 by Th99;
assume not e in G1 .loops() ; :: thesis: contradiction
then A13: v1 <> w1 by A11, GLIB_009:def 2;
then not v2,w2 are_adjacent by A12, Th99;
hence contradiction by A9, A13, CHORD:def 6; :: thesis: verum

end;

then the_Edges_of G1 c= G1 .loops() by TARSKI:def 3;
hence the_Edges_of G1 = G1 .loops() by XBOOLE_0:def 10; :: thesis: verum

end;

thus verum ; :: thesis: verum