set a = the read-write Int-Location;
take the read-write Int-Location := the read-write Int-Location ; :: thesis: ( the read-write Int-Location := the read-write Int-Location is good & the read-write Int-Location := the read-write Int-Location is sequential )
thus ( the read-write Int-Location := the read-write Int-Location is good & the read-write Int-Location := the read-write Int-Location is sequential ) ; :: thesis: verum