theorem Th2: :: SFMASTR3:3

for aa being Int-Location holds not Stop SCM+FSA refers aa