let G2 be DSimpleGraph of G; :: thesis: not G2 is connected
consider E being RepDEdgeSelection of G such that
A2: G2 is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops()) by Def10;
thus not G2 is connected by A2, Th33; :: thesis: verum