[FOM] excluded middle in ZFC

[Robert Black]

Adam Epstein's example of a theorem of ZFC whose proof requires 
application of excluded middle to CH is interesting, but there's 
something I would find more interesting.

It has been held that because of the way in which the universe of 
sets is 'open at the top' or 'indefinitely extensible' or whatever, 
excluded middle shouldn't be applied to sentences which, like GCH (as 
opposed to CH) involve a quantification unbounded by rank.

Is there an interesting and natural theorem of ZFC which, though the 
theorem itself (like Adam's one about Borel sets of reals) can be 
stated with quantifiers bounded in rank, requires for its proof 
application of excluded middle to some sentence (like GCH) about the 
sets 'all the way up'?

(I expect this is an easy question to answer for those who know more 
than I do.)

Robert