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

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