theorem :: GLIB_000:23

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