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