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;

hence G .edgesBetween (G .reachableFrom v) = G .edgesInOut (G .reachableFrom v) by XBOOLE_0:def 10; :: thesis: verum

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)

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;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;

end;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)end;

hence
x in G .edgesBetween (G .reachableFrom v)
; :: thesis: verumper cases
( Sx in G .reachableFrom v or Tx in G .reachableFrom v )
by A1, GLIB_000:28;

end;

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;

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;A3: W is_Walk_from v,Sx by Def5;

now :: thesis: Tx in G .reachableFrom v

then A6:
x in G .edgesInto (G .reachableFrom v)
by A1, GLIB_000:def 26;
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 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

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

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;

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;A8: W is_Walk_from v,Tx by Def5;

now :: thesis: Sx in G .reachableFrom v

then A11:
x in G .edgesOutOf (G .reachableFrom v)
by A1, GLIB_000:def 27;
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 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

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

hence G .edgesBetween (G .reachableFrom v) = G .edgesInOut (G .reachableFrom v) by XBOOLE_0:def 10; :: thesis: verum