theorem :: SCMPDS_8:1

for a being Int_position ex i being Nat st a = intpos i