:: deftheorem defines Edges_In GRAPH_3:def 4 :
for G being Graph
for v being Vertex of G holds Edges_In v = Edges_In (v, the carrier' of G);