let G1 be _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
let G2 be 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
let G be GraphUnion of G1,G2; for v, w being Vertex of G ex e being object st e Joins v,w,G
let v, w be Vertex of G; ex e being object st e Joins v,w,G
the_Edges_of G1 misses the_Edges_of G2
by GLIB_012:def 7;
then A1:
G1 tolerates G2
by Th12;
the_Vertices_of G1 = the_Vertices_of G2
by GLIB_012:def 7;
then
the_Vertices_of G1 = (the_Vertices_of G1) \/ (the_Vertices_of G2)
;
then A2:
( v is Vertex of G1 & w is Vertex of G1 )
by A1, Th25;