theorem Th1: :: SCMPDS_2:2

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