let G be _Graph; :: thesis: for v being Vertex of G holds G .edgesBetween (G .reachableFrom v) = G .edgesInOut (G .reachableFrom v)
let v be Vertex of G; :: thesis: G .edgesBetween (G .reachableFrom v) = G .edgesInOut (G .reachableFrom v)
set R = G .reachableFrom v;

now :: thesis: for x being object st x in G .edgesInOut (G .reachableFrom v) holds
x in G .edgesBetween (G .reachableFrom v)

let x be object ; :: thesis: ( x in G .edgesInOut (G .reachableFrom v) implies x in G .edgesBetween (G .reachableFrom v) )
set Sx = (the_Source_of G) . x;
set Tx = (the_Target_of G) . x;
assume A1: x in G .edgesInOut (G .reachableFrom v) ; :: thesis: x in G .edgesBetween (G .reachableFrom v)
then reconsider Sx = (the_Source_of G) . x, Tx = (the_Target_of G) . x as Vertex of G by FUNCT_2:5;

now :: thesis: x in G .edgesBetween (G .reachableFrom v)

per cases ( Sx in G .reachableFrom v or Tx in G .reachableFrom v ) by A1, GLIB_000:28;

suppose A2: Sx in G .reachableFrom v ; :: thesis: x in G .edgesBetween (G .reachableFrom v)

then consider W being Walk of G such that
A3: W is_Walk_from v,Sx by Def5;

now :: thesis: Tx in G .reachableFrom v

W .last() = Sx by A3, GLIB_001:def 23;
then A4: x Joins W .last() ,Tx,G by A1, GLIB_000:def 13;
assume A5: not Tx in G .reachableFrom v ; :: thesis: contradiction
W .first() = v by A3, GLIB_001:def 23;
then W .addEdge x is_Walk_from v,Tx by A4, GLIB_001:63;
hence contradiction by A5, Def5; :: thesis: verum

end;

then A6: x in G .edgesInto (G .reachableFrom v) by A1, GLIB_000:def 26;
x in G .edgesOutOf (G .reachableFrom v) by A1, A2, GLIB_000:def 27;
then x in (G .edgesInto (G .reachableFrom v)) /\ (G .edgesOutOf (G .reachableFrom v)) by A6, XBOOLE_0:def 4;
hence x in G .edgesBetween (G .reachableFrom v) by GLIB_000:def 29; :: thesis: verum

end;

suppose A7: Tx in G .reachableFrom v ; :: thesis: x in G .edgesBetween (G .reachableFrom v)

then consider W being Walk of G such that
A8: W is_Walk_from v,Tx by Def5;

now :: thesis: Sx in G .reachableFrom v

W .last() = Tx by A8, GLIB_001:def 23;
then A9: x Joins W .last() ,Sx,G by A1, GLIB_000:def 13;
assume A10: not Sx in G .reachableFrom v ; :: thesis: contradiction
W .first() = v by A8, GLIB_001:def 23;
then W .addEdge x is_Walk_from v,Sx by A9, GLIB_001:63;
hence contradiction by A10, Def5; :: thesis: verum

end;

then A11: x in G .edgesOutOf (G .reachableFrom v) by A1, GLIB_000:def 27;
x in G .edgesInto (G .reachableFrom v) by A1, A7, GLIB_000:def 26;
then x in (G .edgesInto (G .reachableFrom v)) /\ (G .edgesOutOf (G .reachableFrom v)) by A11, XBOOLE_0:def 4;
hence x in G .edgesBetween (G .reachableFrom v) by GLIB_000:def 29; :: thesis: verum

end;

end;

end;

hence x in G .edgesBetween (G .reachableFrom v) ; :: thesis: verum

end;

then ( G .edgesBetween (G .reachableFrom v) c= G .edgesInOut (G .reachableFrom v) & G .edgesInOut (G .reachableFrom v) c= G .edgesBetween (G .reachableFrom v) ) by GLIB_000:33;
hence G .edgesBetween (G .reachableFrom v) = G .edgesInOut (G .reachableFrom v) by XBOOLE_0:def 10; :: thesis: verum