theorem :: GLIB_003:31

for G being nonnegative-weighted WGraph
for e being set st e in the_Edges_of G holds
0 <= (the_Weight_of G) . e