theorem :: GRAPH_2:30

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