let H be addLoops of G,V; :: thesis: H is Dcomplete
let v, w be Vertex of H; :: according to GLIB_016:def 1 :: thesis: ( v <> w implies ex e being object st e DJoins v,w,H )
reconsider v9 = v, w9 = w as Vertex of G by GLIB_012:15;
assume A4: v <> w ; :: thesis: ex e being object st e DJoins v,w,H
then consider e being object such that
A5: e DJoins v9,w9,G by Def1;
take e ; :: thesis: e DJoins v,w,H
thus e DJoins v,w,H by A4, A5, GLIB_012:16; :: thesis: verum