let G be _Graph; ( G is non-Dmulti iff for v, w being object holds G .edgesDBetween ({v},{w}) is trivial )
hereby ( ( for v, w being object holds G .edgesDBetween ({v},{w}) is trivial ) implies G is non-Dmulti )
assume A1:
G is
non-Dmulti
;
for v, w being object holds G .edgesDBetween ({v},{w}) is trivial let v,
w be
object ;
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 ;
( e1 in G .edgesDBetween ({v},{w}) & e2 in G .edgesDBetween ({v},{w}) implies e1 = e2 )
assume
e1 in G .edgesDBetween (
{v},
{w})
;
( 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})
;
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;
verum
end; hence
G .edgesDBetween (
{v},
{w}) is
trivial
by ZFMISC_1:def 10;
verum
end;
assume A3:
for v, w being object holds G .edgesDBetween ({v},{w}) is trivial
; G is non-Dmulti
now for e1, e2, v, w being object st e1 DJoins v,w,G & e2 DJoins v,w,G holds
e1 = e2let e1,
e2,
v,
w be
object ;
( 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 )
;
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;
verum end;
hence
G is non-Dmulti
by GLIB_000:def 21; verum