let G2 be SimpleGraph of G; :: thesis: not G2 is connected

consider E being RepEdgeSelection of G such that

A1: G2 is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops()) by Def9;

thus not G2 is connected by A1, Th33; :: thesis: verum

consider E being RepEdgeSelection of G such that

A1: G2 is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops()) by Def9;

thus not G2 is connected by A1, Th33; :: thesis: verum