let G1 be _Graph; :: thesis: for G2 being simple _Graph holds
( G2 is GraphComplement of G1 iff ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & ( for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( v1,w1 are_adjacent iff not v2,w2 are_adjacent ) ) ) )
let G2 be simple _Graph; :: thesis: ( G2 is GraphComplement of G1 iff ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & ( for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( v1,w1 are_adjacent iff not v2,w2 are_adjacent ) ) ) )

hereby :: thesis: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & ( for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( v1,w1 are_adjacent iff not v2,w2 are_adjacent ) ) implies G2 is GraphComplement of G1 )

assume A1: G2 is GraphComplement of G1 ; :: thesis: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & ( for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( ( v1,w1 are_adjacent implies not v2,w2 are_adjacent ) & ( not v2,w2 are_adjacent implies v1,w1 are_adjacent ) ) ) )
hence ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 ) by Th98; :: thesis: for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( ( v1,w1 are_adjacent implies not v2,w2 are_adjacent ) & ( not v2,w2 are_adjacent implies v1,w1 are_adjacent ) )
let v1, w1 be Vertex of G1; :: thesis: for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( ( v1,w1 are_adjacent implies not v2,w2 are_adjacent ) & ( not v2,w2 are_adjacent implies v1,w1 are_adjacent ) )
let v2, w2 be Vertex of G2; :: thesis: ( v1 = v2 & w1 = w2 & v1 <> w1 implies ( ( v1,w1 are_adjacent implies not v2,w2 are_adjacent ) & ( not v2,w2 are_adjacent implies v1,w1 are_adjacent ) ) )
assume A2: ( v1 = v2 & w1 = w2 & v1 <> w1 ) ; :: thesis: ( ( v1,w1 are_adjacent implies not v2,w2 are_adjacent ) & ( not v2,w2 are_adjacent implies v1,w1 are_adjacent ) )

hereby :: thesis: ( not v2,w2 are_adjacent implies v1,w1 are_adjacent )

assume v1,w1 are_adjacent ; :: thesis: not v2,w2 are_adjacent
then ex e1 being object st e1 Joins v1,w1,G1 by CHORD:def 3;
then for e2 being object holds not e2 Joins v1,w1,G2 by A1, A2, Th98;
hence not v2,w2 are_adjacent by A2, CHORD:def 3; :: thesis: verum

end;

assume not v2,w2 are_adjacent ; :: thesis: v1,w1 are_adjacent
then for e2 being object holds not e2 Joins v1,w1,G2 by A2, CHORD:def 3;
then ex e1 being object st e1 Joins v1,w1,G1 by A1, A2, Th98;
hence v1,w1 are_adjacent by CHORD:def 3; :: thesis: verum

end;

assume that
A3: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 ) and
A4: for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( v1,w1 are_adjacent iff not v2,w2 are_adjacent ) ; :: thesis: G2 is GraphComplement of G1

now :: thesis: for v1, w1 being Vertex of G1 st v1 <> w1 holds
( ( ex e1 being object st e1 Joins v1,w1,G1 implies for e2 being object holds not e2 Joins v1,w1,G2 ) & ( ( for e2 being object holds not e2 Joins v1,w1,G2 ) implies ex e1 being object st e1 Joins v1,w1,G1 ) )

let v1, w1 be Vertex of G1; :: thesis: ( v1 <> w1 implies ( ( ex e1 being object st e1 Joins v1,w1,G1 implies for e2 being object holds not e2 Joins v1,w1,G2 ) & ( ( for e2 being object holds not e2 Joins v1,w1,G2 ) implies ex e1 being object st e1 Joins v1,w1,G1 ) ) )
assume A5: v1 <> w1 ; :: thesis: ( ( ex e1 being object st e1 Joins v1,w1,G1 implies for e2 being object holds not e2 Joins v1,w1,G2 ) & ( ( for e2 being object holds not e2 Joins v1,w1,G2 ) implies ex e1 being object st e1 Joins v1,w1,G1 ) )
reconsider v2 = v1, w2 = w1 as Vertex of G2 by A3;

hereby :: thesis: ( ( for e2 being object holds not e2 Joins v1,w1,G2 ) implies ex e1 being object st e1 Joins v1,w1,G1 )

assume ex e1 being object st e1 Joins v1,w1,G1 ; :: thesis: for e2 being object holds not e2 Joins v1,w1,G2
then v1,w1 are_adjacent by CHORD:def 3;
then not v2,w2 are_adjacent by A5, A4;
hence for e2 being object holds not e2 Joins v1,w1,G2 by CHORD:def 3; :: thesis: verum

end;

assume for e2 being object holds not e2 Joins v1,w1,G2 ; :: thesis: ex e1 being object st e1 Joins v1,w1,G1
then not v2,w2 are_adjacent by CHORD:def 3;
then v1,w1 are_adjacent by A5, A4;
hence ex e1 being object st e1 Joins v1,w1,G1 by CHORD:def 3; :: thesis: verum

end;

hence G2 is GraphComplement of G1 by A3, Th98; :: thesis: verum