let G be _Graph; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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})) <> {} ; :: thesis: 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 Def31;
then ( (the_Source_of G) . e in {v} & (the_Source_of G) . e in {w} ) ;
then ( (the_Source_of G) . e = v & (the_Source_of G) . e = w ) by TARSKI:def 1;
hence contradiction by A1; :: thesis: verum

end;

hence G .edgesDBetween ({v},{w}) misses G .edgesDBetween ({w},{v}) by XBOOLE_0:def 7; :: thesis: 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 ; :: thesis: ( e in G .edgesBetween ({v},{w}) iff ( e in G .edgesDBetween ({v},{w}) or e in G .edgesDBetween ({w},{v}) ) )

hereby :: thesis: ( ( 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}) ; :: thesis: ( e in G .edgesDBetween ({v},{w}) or e in G .edgesDBetween ({w},{v}) )
then e SJoins {v},{w},G by Def30;
then ( e DSJoins {v},{w},G or e DSJoins {w},{v},G ) ;
hence ( e in G .edgesDBetween ({v},{w}) or e in G .edgesDBetween ({w},{v}) ) by Def31; :: thesis: verum

end;

assume ( e in G .edgesDBetween ({v},{w}) or e in G .edgesDBetween ({w},{v}) ) ; :: thesis: e in G .edgesBetween ({v},{w})
then ( e DSJoins {v},{w},G or e DSJoins {w},{v},G ) by Def31;
then e SJoins {v},{w},G ;
hence e in G .edgesBetween ({v},{w}) by Def30; :: thesis: verum

end;

hence G .edgesBetween ({v},{w}) = (G .edgesDBetween ({v},{w})) \/ (G .edgesDBetween ({w},{v})) by XBOOLE_0:def 3; :: thesis: verum