theorem Th1: :: HEYTING3:1

for X being non empty finite Subset of NAT ex n being Element of NAT st X c= (Seg n) \/ {0}