let G1 be reverseEdgeDirections of G,E; :: thesis: G1 is non-multi
for e1, e2, v1, v2 being object st e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 holds
e1 = e2

proof

let e1, e2, v1, v2 be object ; :: thesis: ( e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 implies e1 = e2 )
assume ( e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 ) ; :: thesis: e1 = e2
then ( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) by Th9;
hence e1 = e2 by GLIB_000:def 20; :: thesis: verum

end;

hence G1 is non-multi by GLIB_000:def 20; :: thesis: verum