let G be _Graph; :: thesis: ( G is non-Dmulti iff for v, w being object holds G .edgesDBetween ({v},{w}) is trivial )
hereby :: thesis: ( ( for v, w being object holds G .edgesDBetween ({v},{w}) is trivial ) implies G is non-Dmulti )
assume A1: G is non-Dmulti ; :: thesis: for v, w being object holds G .edgesDBetween ({v},{w}) is trivial
let v, w be object ; :: thesis: G .edgesDBetween ({v},{w}) is trivial
for e1, e2 being object st e1 in G .edgesDBetween ({v},{w}) & e2 in G .edgesDBetween ({v},{w}) holds
e1 = e2
proof
let e1, e2 be object ; :: thesis: ( e1 in G .edgesDBetween ({v},{w}) & e2 in G .edgesDBetween ({v},{w}) implies e1 = e2 )
assume e1 in G .edgesDBetween ({v},{w}) ; :: thesis: ( not e2 in G .edgesDBetween ({v},{w}) or e1 = e2 )
then e1 DSJoins {v},{w},G by GLIB_000:def 31;
then A2: e1 DJoins v,w,G by Th13;
assume e2 in G .edgesDBetween ({v},{w}) ; :: thesis: e1 = e2
then e2 DSJoins {v},{w},G by GLIB_000:def 31;
then e2 DJoins v,w,G by Th13;
hence e1 = e2 by A1, A2, GLIB_000:def 21; :: thesis: verum
end;
hence G .edgesDBetween ({v},{w}) is trivial by ZFMISC_1:def 10; :: thesis: verum
end;
assume A3: for v, w being object holds G .edgesDBetween ({v},{w}) is trivial ; :: thesis: G is non-Dmulti
now :: thesis: for e1, e2, v, w being object st e1 DJoins v,w,G & e2 DJoins v,w,G holds
e1 = e2
let e1, e2, v, w be object ; :: thesis: ( e1 DJoins v,w,G & e2 DJoins v,w,G implies e1 = e2 )
assume A4: ( e1 DJoins v,w,G & e2 DJoins v,w,G ) ; :: thesis: e1 = e2
( v in {v} & w in {w} ) by TARSKI:def 1;
then ( e1 DSJoins {v},{w},G & e2 DSJoins {v},{w},G ) by A4, Th7;
then A5: ( e1 in G .edgesDBetween ({v},{w}) & e2 in G .edgesDBetween ({v},{w}) ) by GLIB_000:def 31;
G .edgesDBetween ({v},{w}) is trivial by A3;
hence e1 = e2 by A5, ZFMISC_1:def 10; :: thesis: verum
end;
hence G is non-Dmulti by GLIB_000:def 21; :: thesis: verum