let l be Nat; :: thesis: for a being Int-Location holds not a in dom (Start-At (l,SCM+FSA))
let a be Int-Location; :: thesis: not a in dom (Start-At (l,SCM+FSA))
assume a in dom (Start-At (l,SCM+FSA)) ; :: thesis: contradiction
then a = IC by TARSKI:def 1;
hence contradiction by Th49; :: thesis: verum