let G3 be DSimpleGraph of G; :: thesis: G3 is complete
consider G2 being removeDParallelEdges of G such that
A2: G3 is removeLoops of G2 by Th120;
thus G3 is complete by A2; :: thesis: verum