let G3 be DSimpleGraph of G; :: thesis: ( G3 is spanning & G3 is loopless & G3 is non-Dmulti & G3 is Dsimple )
consider E being RepDEdgeSelection of G such that
A3: G3 is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops()) by Def10;
consider G2 being removeDParallelEdges of G such that
A4: G3 is removeLoops of G2 by Th120;
thus ( G3 is spanning & G3 is loopless & G3 is non-Dmulti & G3 is Dsimple ) by A3, A4; :: thesis: verum