let G1 be reverseEdgeDirections of G,E; 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 ;
( e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 implies e1 = e2 )
assume
(
e1 Joins v1,
v2,
G1 &
e2 Joins v1,
v2,
G1 )
;
e1 = e2
then
(
e1 Joins v1,
v2,
G &
e2 Joins v1,
v2,
G )
by Th9;
hence
e1 = e2
by GLIB_000:def 20;
verum
end;
hence
G1 is non-multi
by GLIB_000:def 20; verum