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

per cases ( ex e1 being object st e1 Joins v,w,G1 or for e1 being object holds not e1 Joins v,w,G1 ) ;

suppose ex e1 being object st e1 Joins v,w,G1 ; :: thesis: ex e being object st e Joins v,w,G

then consider e1 being object such that
A4: e1 Joins v,w,G1 ;
take e1 ; :: thesis: e1 Joins v,w,G
thus e1 Joins v,w,G by A4, GLIB_006:70; :: thesis: verum

end;

suppose for e1 being object holds not e1 Joins v,w,G1 ; :: thesis: ex e being object st e Joins v,w,G

then consider e2 being object such that
A5: e2 Joins v,w,G2 by A1, A3, GLIB_012:98;
take e2 ; :: thesis: e2 Joins v,w,G
G is Supergraph of G2 by A2, Th26;
hence e2 Joins v,w,G by A5, GLIB_006:70; :: thesis: verum

end;

end;