theorem :: GRAPH_4:2

for e being set
for G being Graph
for v1, v2, v3, v4 being Element of G st e orientedly_joins v1,v2 & e orientedly_joins v3,v4 holds
( v1 = v3 & v2 = v4 ) ;