 The statement \(\forall \bx_{\alpha}\bA_{{o}}\) is true iff the set \([\lambda \bx_{\alpha}\bA_{{o}}]\) contains all elements of type α. A constant \(\Pi_{{o}({o}\alpha)}\) can be introduced (for each type symbol \(\alpha)\) to denote a property of sets: a set \(s_{{o}\alpha}\) has the property \(\Pi_{{o}({o}\alpha)}\) iff \(s_{{o}\alpha}\) contains all elements of type α. With this interpretation 