theorem :: GLIB_000:23

for G being loopless trivial _Graph holds the_Edges_of G = {}