:: deftheorem Def9 defines SimpleGraph GLIB_009:def 9 :
for G being _Graph
for b₂ being Subgraph of G holds
( b₂ is SimpleGraph of G iff ex E being RepEdgeSelection of G st b₂ is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops()) );