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 4;
then A1: (the_Weight_of G) . e in rng (the_Weight_of G) by FUNCT_1:12;
rng (the_Weight_of G) c= Real>=0 by Def14;
then (the_Weight_of G) . e in Real>=0 by A1;
then consider r being Real such that
A2: ( (the_Weight_of G) . e = r & r >= 0 ) by GRAPH_5:def 12;
thus 0 <= (the_Weight_of G) . e by A2; :: thesis: verum