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 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; :: 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 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; :: 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 GLIB_000:def 31;
then e SJoins {v},{w},G by Th11;
hence e in G .edgesBetween ({v},{w}) by GLIB_000:def 30; :: thesis: verum
end;
hence G .edgesBetween ({v},{w}) = (G .edgesDBetween ({v},{w})) \/ (G .edgesDBetween ({w},{v})) by XBOOLE_0:def 3; :: thesis: verum