theorem :: SCMPDS_4:18

for a being Int_position
for l being Nat holds not a in dom (Start-At (l,SCMPDS))