take i = the read-write Int-Location := (intloc 1); :: thesis: ( i is keeping_0 & i is sequential )
thus i is keeping_0 ; :: thesis: i is sequential
thus i is sequential ; :: thesis: verum