SUCC (inspos 2) = NAT by Th24;
then A1: inspos 2 <= inspos 1 by AMISTD_1:59;
SUCC (inspos 1) = NAT by Th24;
then A2: inspos 1 <= inspos 2 by AMISTD_1:59;
assume SCMPDS is InsLoc-antisymmetric ; :: thesis: contradiction
hence contradiction by A2, A1, AMISTD_1:def 9; :: thesis: verum