let a be Int_position ; :: thesis: for l being Instruction-Location of SCMPDS holds not a in dom (Start-At l)
let l be Instruction-Location of SCMPDS ; :: thesis: not a in dom (Start-At l)
assume A1: a in dom (Start-At l) ; :: thesis: contradiction
dom (Start-At l) = {(IC SCMPDS )} by FUNCOP_1:19;
then a = IC SCMPDS by A1, TARSKI:def 1;
hence contradiction by SCMPDS_2:52; :: thesis: verum