let G1 be _Graph; :: thesis: for G2 being DLGraphComplement of G1
for G being GraphUnion of G1,G2
for v, w being Vertex of G ex e being object st e DJoins v,w,G
let G2 be DLGraphComplement of G1; :: thesis: for G being GraphUnion of G1,G2
for v, w being Vertex of G ex e being object st e DJoins v,w,G
let G be GraphUnion of G1,G2; :: thesis: for v, w being Vertex of G ex e being object st e DJoins v,w,G
let v, w be Vertex of G; :: thesis: ex e being object st e DJoins v,w,G
the_Edges_of G1 misses the_Edges_of G2 by GLIB_012:def 6;
then A1: G1 tolerates G2 by Th12;
the_Vertices_of G1 = the_Vertices_of G2 by GLIB_012:def 6;
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;

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

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

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

end;

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

then consider e2 being object such that
A4: e2 DJoins v,w,G2 by A2, GLIB_012:def 6;
take e2 ; :: thesis: e2 DJoins v,w,G
G is Supergraph of G2 by A1, Th26;
hence e2 DJoins v,w,G by A4, GLIB_006:70; :: thesis: verum

end;

end;