let G be oriented Graph; :: thesis: for v1, v2 being Vertex of G
for e1, e2 being set st e1 in the carrier' of G & e2 in the carrier' of G & e1 orientedly_joins v1,v2 & e2 orientedly_joins v1,v2 holds
e1 = e2
let v1, v2 be Vertex of G; :: thesis: for e1, e2 being set st e1 in the carrier' of G & e2 in the carrier' of G & e1 orientedly_joins v1,v2 & e2 orientedly_joins v1,v2 holds
e1 = e2
let e1, e2 be set ; :: thesis: ( e1 in the carrier' of G & e2 in the carrier' of G & e1 orientedly_joins v1,v2 & e2 orientedly_joins v1,v2 implies e1 = e2 )
assume A1: ( e1 in the carrier' of G & e2 in the carrier' of G & e1 orientedly_joins v1,v2 & e2 orientedly_joins v1,v2 ) ; :: thesis: e1 = e2
then ( the Source of G . e1 = v1 & the Target of G . e1 = v2 & the Source of G . e2 = v1 & the Target of G . e2 = v2 ) by GRAPH_4:def 1;
hence e1 = e2 by A1, GRAPH_1:def 5; :: thesis: verum