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 that
A1: ( e1 in the carrier' of G & e2 in the carrier' of G ) and
A2: e1 orientedly_joins v1,v2 and
A3: e2 orientedly_joins v1,v2 ; :: thesis: e1 = e2
A4: ( the Source of G . e2 = v1 & the Target of G . e2 = v2 ) by A3, GRAPH_4:def 1;
( the Source of G . e1 = v1 & the Target of G . e1 = v2 ) by A2, GRAPH_4:def 1;
hence e1 = e2 by A1, A4, GRAPH_1:def 7; :: thesis: verum