:: deftheorem defines IC SCMRING1:def 4 :
for G being non empty 1-sorted
for s being SCM-State of G holds IC s = s . NAT;