:: deftheorem defines IC AMI_2:def 6 :
for s being SCM-State holds IC s = s . NAT;