theorem Th1: :: AFINSQ_2:1

for i being Nat
for x being object st x in i holds
x is Element of NAT