:: deftheorem Def2 defines read-only SCMFSA_M:def 2 :
for IT being Int-Location holds
( IT is read-only iff IT = intloc 0 );