theorem :: GRAPHSP:24

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) = - 1 iff for e being set holds
( not e in the carrier' of G or not e orientedly_joins v1,v2 ) ) by Def7, Th23;