let G1 be Dsimple _Graph; :: thesis: for G2 being DGraphComplement of G1 holds G1 is DGraphComplement of G2
let G2 be DGraphComplement of G1; :: thesis: G1 is DGraphComplement of G2
A1: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 misses the_Edges_of G2 ) by Th80;

now :: thesis: for v, w being Vertex of G2 st v <> w holds
( ex e2 being object st e2 DJoins v,w,G2 iff for e1 being object holds not e1 DJoins v,w,G1 )

let v, w be Vertex of G2; :: thesis: ( v <> w implies ( ex e2 being object st e2 DJoins v,w,G2 iff for e1 being object holds not e1 DJoins v,w,G1 ) )
assume A2: v <> w ; :: thesis: ( ex e2 being object st e2 DJoins v,w,G2 iff for e1 being object holds not e1 DJoins v,w,G1 )
( v is Vertex of G1 & w is Vertex of G1 ) by Th80;
hence ( ex e2 being object st e2 DJoins v,w,G2 iff for e1 being object holds not e1 DJoins v,w,G1 ) by A2, Th80; :: thesis: verum

end;

hence G1 is DGraphComplement of G2 by A1, Th80; :: thesis: verum