for p being Program of
for s being State of SCM+FSA holds (UsedI*Loc p) \/ (UsedILoc p) c= dom s