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