theorem Th3: :: GRAPH_5:3

for D being finite set
for n being Element of NAT
for X being set st X = { x where x is Element of D * : len x <= n } holds
X is finite