let G be _Graph; :: thesis: for X being set st X /\ (the_Vertices_of G) = {} holds
( G .edgesInto X = {} & G .edgesOutOf X = {} & G .edgesInOut X = {} & G .edgesBetween X = {} )
let X be set ; :: thesis: ( X /\ (the_Vertices_of G) = {} implies ( G .edgesInto X = {} & G .edgesOutOf X = {} & G .edgesInOut X = {} & G .edgesBetween X = {} ) )
assume A1: X /\ (the_Vertices_of G) = {} ; :: thesis: ( G .edgesInto X = {} & G .edgesOutOf X = {} & G .edgesInOut X = {} & G .edgesBetween X = {} )
thus A2: G .edgesInto X = {} :: thesis: ( G .edgesOutOf X = {} & G .edgesInOut X = {} & G .edgesBetween X = {} )

proof

assume A3: G .edgesInto X <> {} ; :: thesis: contradiction
set e = the Element of G .edgesInto X;
A4: ( the Element of G .edgesInto X in the_Edges_of G & (the_Target_of G) . the Element of G .edgesInto X in X ) by Def26, A3;
then the Element of G .edgesInto X Joins (the_Source_of G) . the Element of G .edgesInto X,(the_Target_of G) . the Element of G .edgesInto X,G ;
then (the_Target_of G) . the Element of G .edgesInto X in the_Vertices_of G by FUNCT_2:5;
hence contradiction by A1, A4, XBOOLE_0:def 4; :: thesis: verum

end;

thus A5: G .edgesOutOf X = {} :: thesis: ( G .edgesInOut X = {} & G .edgesBetween X = {} )

proof

assume A6: G .edgesOutOf X <> {} ; :: thesis: contradiction
set e = the Element of G .edgesOutOf X;
A7: ( the Element of G .edgesOutOf X in the_Edges_of G & (the_Source_of G) . the Element of G .edgesOutOf X in X ) by A6, Def27;
then the Element of G .edgesOutOf X Joins (the_Source_of G) . the Element of G .edgesOutOf X,(the_Target_of G) . the Element of G .edgesOutOf X,G ;
then (the_Source_of G) . the Element of G .edgesOutOf X in the_Vertices_of G by FUNCT_2:5;
hence contradiction by A1, A7, XBOOLE_0:def 4; :: thesis: verum

end;

thus G .edgesInOut X = {} by A2, A5; :: thesis: G .edgesBetween X = {}
thus G .edgesBetween X = {} by A2; :: thesis: verum