let G be _Graph; for v, w being object st v <> w holds
( G .edgesDBetween ({v},{w}) misses G .edgesDBetween ({w},{v}) & G .edgesBetween ({v},{w}) = (G .edgesDBetween ({v},{w})) \/ (G .edgesDBetween ({w},{v})) )
let v, w be object ; ( v <> w implies ( G .edgesDBetween ({v},{w}) misses G .edgesDBetween ({w},{v}) & G .edgesBetween ({v},{w}) = (G .edgesDBetween ({v},{w})) \/ (G .edgesDBetween ({w},{v})) ) )
assume A1:
v <> w
; ( G .edgesDBetween ({v},{w}) misses G .edgesDBetween ({w},{v}) & G .edgesBetween ({v},{w}) = (G .edgesDBetween ({v},{w})) \/ (G .edgesDBetween ({w},{v})) )
(G .edgesDBetween ({v},{w})) /\ (G .edgesDBetween ({w},{v})) = {}
proof
assume
(G .edgesDBetween ({v},{w})) /\ (G .edgesDBetween ({w},{v})) <> {}
;
contradiction
then consider e being
object such that A2:
e in (G .edgesDBetween ({v},{w})) /\ (G .edgesDBetween ({w},{v}))
by XBOOLE_0:def 1;
(
e in G .edgesDBetween (
{v},
{w}) &
e in G .edgesDBetween (
{w},
{v}) )
by A2, XBOOLE_0:def 4;
then
(
e DSJoins {v},
{w},
G &
e DSJoins {w},
{v},
G )
by GLIB_000:def 31;
then
(
(the_Source_of G) . e in {v} &
(the_Source_of G) . e in {w} )
by GLIB_000:def 16;
then
(
(the_Source_of G) . e = v &
(the_Source_of G) . e = w )
by TARSKI:def 1;
hence
contradiction
by A1;
verum
end;
hence
G .edgesDBetween ({v},{w}) misses G .edgesDBetween ({w},{v})
by XBOOLE_0:def 7; G .edgesBetween ({v},{w}) = (G .edgesDBetween ({v},{w})) \/ (G .edgesDBetween ({w},{v}))
for e being object holds
( e in G .edgesBetween ({v},{w}) iff ( e in G .edgesDBetween ({v},{w}) or e in G .edgesDBetween ({w},{v}) ) )
proof
let e be
object ;
( e in G .edgesBetween ({v},{w}) iff ( e in G .edgesDBetween ({v},{w}) or e in G .edgesDBetween ({w},{v}) ) )
hereby ( ( e in G .edgesDBetween ({v},{w}) or e in G .edgesDBetween ({w},{v}) ) implies e in G .edgesBetween ({v},{w}) )
assume
e in G .edgesBetween (
{v},
{w})
;
( e in G .edgesDBetween ({v},{w}) or e in G .edgesDBetween ({w},{v}) )then
e SJoins {v},
{w},
G
by GLIB_000:def 30;
then
(
e DSJoins {v},
{w},
G or
e DSJoins {w},
{v},
G )
by Th11;
hence
(
e in G .edgesDBetween (
{v},
{w}) or
e in G .edgesDBetween (
{w},
{v}) )
by GLIB_000:def 31;
verum
end;
assume
(
e in G .edgesDBetween (
{v},
{w}) or
e in G .edgesDBetween (
{w},
{v}) )
;
e in G .edgesBetween ({v},{w})
then
(
e DSJoins {v},
{w},
G or
e DSJoins {w},
{v},
G )
by GLIB_000:def 31;
then
e SJoins {v},
{w},
G
by Th11;
hence
e in G .edgesBetween (
{v},
{w})
by GLIB_000:def 30;
verum
end;
hence
G .edgesBetween ({v},{w}) = (G .edgesDBetween ({v},{w})) \/ (G .edgesDBetween ({w},{v}))
by XBOOLE_0:def 3; verum