for G1 being _Graph
for G2 being GraphComplement of G1
for G being GraphUnion of G1,G2
for v, w being Vertex of G st v <> w holds
ex e being object st e Joins v,w,G