theorem :: AMI_3:29

for s being SCM-State holds s is State of SCM by Lm1;