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;

thus ( Weight (v1,v2,W) >= 0 implies ex e being set st

( e in the carrier' of G & e orientedly_joins v1,v2 ) ) by Def7; :: thesis: ( ex e being set st

( e in the carrier' of G & e orientedly_joins v1,v2 ) implies Weight (v1,v2,W) >= 0 )

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

A1: XEdge (v1,v2) = e and

A2: e in the carrier' of G and

A3: e orientedly_joins v1,v2 by Def6;

e in dom W by A2, FUNCT_2:def 1;

then W . e in Real>=0 by PARTFUN1:4;

then ex r being Real st

( W . e = r & r >= 0 ) by GRAPH_5:def 12;

hence Weight (v1,v2,W) >= 0 by A1, A2, A3, Def7; :: thesis: verum

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;

thus ( Weight (v1,v2,W) >= 0 implies ex e being set st

( e in the carrier' of G & e orientedly_joins v1,v2 ) ) by Def7; :: thesis: ( ex e being set st

( e in the carrier' of G & e orientedly_joins v1,v2 ) implies Weight (v1,v2,W) >= 0 )

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

A1: XEdge (v1,v2) = e and

A2: e in the carrier' of G and

A3: e orientedly_joins v1,v2 by Def6;

e in dom W by A2, FUNCT_2:def 1;

then W . e in Real>=0 by PARTFUN1:4;

then ex r being Real st

( W . e = r & r >= 0 ) by GRAPH_5:def 12;

hence Weight (v1,v2,W) >= 0 by A1, A2, A3, Def7; :: thesis: verum