let G be _Graph; :: thesis: for X being set holds G .edgesBetween X c= G .edgesInOut X
let X be set ; :: thesis: G .edgesBetween X c= G .edgesInOut X

now

let z be set ; :: thesis: ( z in G .edgesBetween X implies z in G .edgesInOut X )
assume z in G .edgesBetween X ; :: thesis: z in G .edgesInOut X
then z in G .edgesInto X by XBOOLE_0:def 4;
hence z in G .edgesInOut X by XBOOLE_0:def 3; :: thesis: verum

end;

hence G .edgesBetween X c= G .edgesInOut X by TARSKI:def 3; :: thesis: verum