 The inference rules of \(\bRA^*\) comprise those of the sequent calculus with the exception of \((\forall R)\) and \((\exists L)\) which are replaced by those for the \(\omega\)-rule: \(\omega\)R and \(\omega\)L. Below \(\fP_{\beta}\) stands for the set of all abstraction terms with levels \(&lt;\beta\). The rules for the set quantifiers are as follows: 