let G1 be _Graph; :: thesis: for G2 being DSimpleGraph of G1
for G3 being DGraphComplement of G1 holds G3 is DGraphComplement of G2
let G2 be DSimpleGraph of G1; :: thesis: for G3 being DGraphComplement of G1 holds G3 is DGraphComplement of G2
let G3 be DGraphComplement of G1; :: thesis: G3 is DGraphComplement of G2
consider E being RepDEdgeSelection of G1 such that
A1: G2 is inducedSubgraph of G1, the_Vertices_of G1,E \ (G1 .loops()) by GLIB_009:def 10;
( the_Vertices_of G1 c= the_Vertices_of G1 & the_Edges_of G1 = G1 .edgesBetween (the_Vertices_of G1) ) by GLIB_000:34;
then A2: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = E \ (G1 .loops()) ) by A1, GLIB_000:def 37;
then A3: the_Vertices_of G3 = the_Vertices_of G2 by Th80;
the_Edges_of G3 misses the_Edges_of G1 by Th80;
then A4: the_Edges_of G3 misses the_Edges_of G2 by XBOOLE_1:63;

now :: thesis: for v, w being Vertex of G2 st v <> w holds
( ( ex e2 being object st e2 DJoins v,w,G2 implies for e3 being object holds not e3 DJoins v,w,G3 ) & ( ( for e3 being object holds not e3 DJoins v,w,G3 ) implies ex e2 being object st e2 DJoins v,w,G2 ) )

let v, w be Vertex of G2; :: thesis: ( v <> w implies ( ( ex e2 being object st e2 DJoins v,w,G2 implies for e3 being object holds not e3 DJoins v,w,G3 ) & ( ( for e3 being object holds not e3 DJoins v,w,G3 ) implies ex e2 being object st e2 DJoins v,w,G2 ) ) )
assume A5: v <> w ; :: thesis: ( ( ex e2 being object st e2 DJoins v,w,G2 implies for e3 being object holds not e3 DJoins v,w,G3 ) & ( ( for e3 being object holds not e3 DJoins v,w,G3 ) implies ex e2 being object st e2 DJoins v,w,G2 ) )
A6: ( v is Vertex of G1 & w is Vertex of G1 ) by GLIB_000:def 33;
reconsider v1 = v, w1 = w as Vertex of G1 by GLIB_000:def 33;

hereby :: thesis: ( ( for e3 being object holds not e3 DJoins v,w,G3 ) implies ex e2 being object st e2 DJoins v,w,G2 )

given e2 being object such that A7: e2 DJoins v,w,G2 ; :: thesis: for e3 being object holds not e3 DJoins v,w,G3
A8: e2 DJoins v,w,G1 by A7, GLIB_000:72;
given e3 being object such that A9: e3 DJoins v,w,G3 ; :: thesis: contradiction
thus contradiction by A8, A9, Th81; :: thesis: verum

end;

assume for e3 being object holds not e3 DJoins v,w,G3 ; :: thesis: ex e2 being object st e2 DJoins v,w,G2
then consider e1 being object such that
A10: e1 DJoins v,w,G1 by A6, A5, Th80;
consider e2 being object such that
A11: ( e2 DJoins v,w,G1 & e2 in E ) and
for e9 being object st e9 DJoins v,w,G1 & e9 in E holds
e9 = e2 by A10, GLIB_009:def 6;
take e2 = e2; :: thesis: e2 DJoins v,w,G2
e2 Joins v,w,G1 by A11, GLIB_000:16;
then not e2 in G1 .loops() by A5, GLIB_009:46;
then e2 in the_Edges_of G2 by A2, A11, XBOOLE_0:def 5;
hence e2 DJoins v,w,G2 by A11, GLIB_000:73; :: thesis: verum

end;

hence G3 is DGraphComplement of G2 by A3, A4, Th80; :: thesis: verum