Summary: The cut-elimination technique is well developed for classical higher-order systems, but, since the normal form (not normalization) theorem was established by Mints, not much further progress has been achieved for logical systems with an $ε$-symbol. We give a cut-elimination procedure for second-order propositional logic with Hilbert’s $ε$-symbol, extensionality and full comprehension. We prove that selective elimination of the $ε$-symbol and quantifiers is possible, so that a cut formula becomes essentially quantifier- and epsilon-free, after which cuts can be eliminated by the standard Gentzen procedure.