theorem Th31: :: GLIB_014:31

for G1 being _Graph
for G2 being LGraphComplement of G1
for G being GraphUnion of G1,G2
for v, w being Vertex of G ex e being object st e Joins v,w,G