SUCC (2,SCMPDS) = NAT by Th18;
then A1: 2 <= 1, SCMPDS by AMI_WSTD:33;
SUCC (1,SCMPDS) = NAT by Th18;
then A2: 1 <= 2, SCMPDS by AMI_WSTD:33;
assume SCMPDS is InsLoc-antisymmetric ; :: thesis: contradiction
hence contradiction by A2, A1, AMI_WSTD:def 2; :: thesis: verum