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 GLIB_000:def 26, 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 by GLIB_000:def 13;
then (the_Target_of G) . the Element of G .edgesInto X in the_Vertices_of G by GLIB_000:13;
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, GLIB_000:def 27;
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 by GLIB_000:def 13;
then (the_Source_of G) . the Element of G .edgesOutOf X in the_Vertices_of G by GLIB_000:13;
hence contradiction by A1, A7, XBOOLE_0:def 4; :: thesis: verum
end;
thus G .edgesInOut X = (G .edgesInto X) \/ (G .edgesOutOf X) by GLIB_000:def 28
.= {} by A2, A5 ; :: thesis: G .edgesBetween X = {}
thus G .edgesBetween X = (G .edgesInto X) /\ (G .edgesOutOf X) by GLIB_000:def 29
.= {} by A2 ; :: thesis: verum