let s be State of SCMPDS ; :: thesis: for d being Int_position holds d in dom s
let d be Int_position ; :: thesis: d in dom s
dom s = the carrier of SCMPDS by AMI_1:79;
hence d in dom s ; :: thesis: verum