for R being Ring
for s being State of (SCM R)
for S being SCM-State of R st S = s holds
IC s = IC S by Def1;