:: deftheorem defines orientedly_joins GRAPH_4:def 1 :
for G being Graph
for x, y being Element of G
for e being set holds
( e orientedly_joins x,y iff ( the Source of G . e = x & the Target of G . e = y ) );