let G2 be _Graph; :: thesis: for E being set
for G1 being reverseEdgeDirections of G2,E st E c= the_Edges_of G2 & G2 is non-Dmulti & ( for e1, e2, v1, v2 being object st e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 & not ( e1 in E & e2 in E ) holds
( not e1 in E & not e2 in E ) ) holds
G1 is non-Dmulti
let E be set ; :: thesis: for G1 being reverseEdgeDirections of G2,E st E c= the_Edges_of G2 & G2 is non-Dmulti & ( for e1, e2, v1, v2 being object st e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 & not ( e1 in E & e2 in E ) holds
( not e1 in E & not e2 in E ) ) holds
G1 is non-Dmulti
let G1 be reverseEdgeDirections of G2,E; :: thesis: ( E c= the_Edges_of G2 & G2 is non-Dmulti & ( for e1, e2, v1, v2 being object st e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 & not ( e1 in E & e2 in E ) holds
( not e1 in E & not e2 in E ) ) implies G1 is non-Dmulti )
assume that
A1: E c= the_Edges_of G2 and
A2: G2 is non-Dmulti and
A3: for e1, e2, v1, v2 being object st e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 & not ( e1 in E & e2 in E ) holds
( not e1 in E & not e2 in E ) ; :: thesis: G1 is non-Dmulti
for e1, e2, v1, v2 being object st e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 holds
e1 = e2

proof

let e1, e2, v1, v2 be object ; :: thesis: ( e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 implies e1 = e2 )
assume A4: ( e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 ) ; :: thesis: e1 = e2
then ( e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 ) by GLIB_000:16;
then ( e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 ) by Th9;

per cases then ( ( e1 in E & e2 in E ) or ( not e1 in E & not e2 in E ) ) by A3;

suppose ( e1 in E & e2 in E ) ; :: thesis: e1 = e2

then ( e1 DJoins v2,v1,G2 & e2 DJoins v2,v1,G2 ) by A1, A4, Th7;
hence e1 = e2 by A2, GLIB_000:def 21; :: thesis: verum

end;

suppose ( not e1 in E & not e2 in E ) ; :: thesis: e1 = e2

then ( e1 DJoins v1,v2,G2 & e2 DJoins v1,v2,G2 ) by A1, A4, Th8;
hence e1 = e2 by A2, GLIB_000:def 21; :: thesis: verum

end;

end;

end;

hence G1 is non-Dmulti by GLIB_000:def 21; :: thesis: verum