theorem Th30: :: GRAPH_3:30

for X being set
for G being finite Graph
for v being Vertex of G holds
( Edges_In (v,X) = Edges_In (v,(X /\ the carrier' of G)) & Edges_Out (v,X) = Edges_Out (v,(X /\ the carrier' of G)) )