:: deftheorem Def6 defines is_forward_edge_wrt GLIB_005:def 6 :
for G being real-weighted WGraph
for EL being FF:ELabeling of G
for VL being AP:VLabeling of EL
for e being set holds
( e is_forward_edge_wrt VL iff ( e in the_Edges_of G & (the_Source_of G) . e in dom VL & not (the_Target_of G) . e in dom VL & EL . e < (the_Weight_of G) . e ) );