theorem Th3: :: HEYTING3:3

for k being Element of NAT
for X being non empty finite Subset of [:NAT,{k}:] ex n being non zero Element of NAT st X c= [:((Seg n) \/ {0}),{k}:]