:: deftheorem defines IC SCMFSA_1:def 15 :
for s being SCM+FSA-State holds IC s = s . NAT;