theorem Th1: :: AMI_3:1

IC = NAT by AMI_2:22, SUBSET_1:def 8;