let G3 be SimpleGraph of G; :: thesis: ( G3 is spanning & G3 is loopless & G3 is non-multi & G3 is simple )
consider E being RepEdgeSelection of G such that
A1: G3 is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops()) by Def9;
consider G2 being removeParallelEdges of G such that
A2: G3 is removeLoops of G2 by Th119;
thus ( G3 is spanning & G3 is loopless & G3 is non-multi & G3 is simple ) by A1, A2; :: thesis: verum