take intloc 1 ; :: thesis: intloc 1 is read-write
intloc 1 <> intloc 0 by AMI_3:10;
hence intloc 1 is read-write ; :: thesis: verum