theorem Th17: :: GRAPH_3:17

for G being Graph
for e, X being set st e in the carrier' of G & e in X holds
not G -VSet X is empty