:: deftheorem Def7 defines is_backward_edge_wrt GLIB_005:def 7 :
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_backward_edge_wrt VL iff ( e in the_Edges_of G & (the_Target_of G) . e in dom VL & not (the_Source_of G) . e in dom VL & 0 < EL . e ) );