let G be oriented Graph; :: thesis: 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 ) )
let v1, v2 be Vertex of G; :: thesis: 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 ) )
let W be Function of the carrier' of G,Real>=0; :: thesis: ( Weight (v1,v2,W) >= 0 iff ex e being set st
( e in the carrier' of G & e orientedly_joins v1,v2 ) )
set EG = the carrier' of G;

hereby :: thesis: ( ex e being set st
( e in the carrier' of G & e orientedly_joins v1,v2 ) implies Weight (v1,v2,W) >= 0 )

assume A1: Weight (v1,v2,W) >= 0 ; :: thesis: ex e being set st
( e in the carrier' of G & e orientedly_joins v1,v2 )
assume for e being set holds
( not e in the carrier' of G or not e orientedly_joins v1,v2 ) ; :: thesis: contradiction
then Weight (v1,v2,W) = - 1 by Def7;
hence contradiction by A1; :: thesis: verum

end;

assume ex e being set st
( e in the carrier' of G & e orientedly_joins v1,v2 ) ; :: thesis: Weight (v1,v2,W) >= 0
then consider e being set such that
A2: XEdge (v1,v2) = e and
A3: e in the carrier' of G and
A4: e orientedly_joins v1,v2 by Def6;
e in dom W by A3, FUNCT_2:def 1;
then W . e in Real>=0 by PARTFUN1:27;
then ex r being Real st
( W . e = r & r >= 0 ) by GRAPH_5:def 12;
hence Weight (v1,v2,W) >= 0 by A2, A3, A4, Def7; :: thesis: verum