theorem :: SCMFSA_2:101

for i, j being Nat st i <> j holds
intloc i <> intloc j by AMI_3:10;