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
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in G .edgesBetween X or 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