let G be _Graph; :: thesis: for X being set holds
( G .edgesInto X c= G .edgesInOut X & G .edgesOutOf X c= G .edgesInOut X )
let X be set ; :: thesis: ( G .edgesInto X c= G .edgesInOut X & G .edgesOutOf X c= G .edgesInOut X )
for z being set st z in G .edgesInto X holds
z in G .edgesInOut X by XBOOLE_0:def 3;
hence G .edgesInto X c= G .edgesInOut X by TARSKI:def 3; :: thesis: G .edgesOutOf X c= G .edgesInOut X
for z being set st z in G .edgesOutOf X holds
z in G .edgesInOut X by XBOOLE_0:def 3;
hence G .edgesOutOf X c= G .edgesInOut X by TARSKI:def 3; :: thesis: verum