let G3 be SimpleGraph of G; :: thesis: G3 is complete
consider G2 being removeParallelEdges of G such that
A1: G3 is removeLoops of G2 by Th119;
thus G3 is complete by A1; :: thesis: verum