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

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