let G be nonnegative-weighted WGraph; :: thesis: for e being set st e in the_Edges_of G holds
0 <= (the_Weight_of G) . e
let e be set ; :: thesis: ( e in the_Edges_of G implies 0 <= (the_Weight_of G) . e )
assume e in the_Edges_of G ; :: thesis: 0 <= (the_Weight_of G) . e
then e in dom (the_Weight_of G) by PARTFUN1:def 2;
then A1: (the_Weight_of G) . e in rng (the_Weight_of G) by FUNCT_1:3;
rng (the_Weight_of G) c= Real>=0 by Def14;
then (the_Weight_of G) . e in Real>=0 by A1;
then ex r being Real st
( (the_Weight_of G) . e = r & r >= 0 ) by GRAPH_5:def 12;
hence 0 <= (the_Weight_of G) . e ; :: thesis: verum