theorem Th25: :: GRAPH_3:25

for X being set
for G being finite Graph
for v being Vertex of G st Degree (v,X) <> 0 holds
not Edges_At (v,X) is empty