for G being oriented Graph
for v1, v2 being Vertex of G
for W being Function of the carrier' of G,Real>=0 holds
( Weight (v1,v2,W) >= 0 iff ex e being set st
( e in the carrier' of G & e orientedly_joins v1,v2 ) )