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