  is the direct counterpart of AC1 in this strengthened second-order language. In words, AC1L asserts that, if each predicate having a certain property \(\Phi\) has instances, then there is a function \(F\) on predicates such that, for any predicate \(X\) satisfying \(\Phi\), \(FX\) is an instance of \(X\). Here predicates are playing the role of sets.