theorem Th1: :: GRAPH_4:1

for e being set
for G being Graph
for v1, v2 being Element of G st e orientedly_joins v1,v2 holds
e joins v1,v2 by GRAPH_1:def 12;