theorem :: GLIB_000:24

for G being _Graph st the_Edges_of G = {} holds
G is simple