let H be addEdge of G,v,e,w; :: thesis: H is Dcomplete

per cases ( ( v in the_Vertices_of G & w in the_Vertices_of G & not e in the_Edges_of G ) or not v in the_Vertices_of G or not w in the_Vertices_of G or e in the_Edges_of G ) ;

suppose ( v in the_Vertices_of G & w in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis: H is Dcomplete

then A1: the_Vertices_of G = the_Vertices_of H by GLIB_006:def 11;
let v1, w1 be Vertex of H; :: according to GLIB_016:def 1 :: thesis: ( v1 <> w1 implies ex e being object st e DJoins v1,w1,H )
reconsider v2 = v1, w2 = w1 as Vertex of G by A1;
assume v1 <> w1 ; :: thesis: ex e being object st e DJoins v1,w1,H
then consider e being object such that
A2: e DJoins v2,w2,G by Def1;
take e ; :: thesis: e DJoins v1,w1,H
thus e DJoins v1,w1,H by A2, GLIB_006:70; :: thesis: verum

end;

suppose ( not v in the_Vertices_of G or not w in the_Vertices_of G or e in the_Edges_of G ) ; :: thesis: H is Dcomplete

then G == H by GLIB_006:def 11;
hence H is Dcomplete by Th4; :: thesis: verum

end;

end;