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