I'm looking for a reference to the statement that Lawvere's [Elementary Theory of the Category of Sets (ETCS)](http://www.tac.mta.ca/tac/reprints/articles/11/tr11abs.html) is equivalent in proof-theoretic strength to finite order arithmetic.  The person who informed me of this said it was well-known in certain circles, but he couldn't think of a reference.

Actually, all I need is a reference to one half of the equivalence: that anything provable in finite order arithmetic is provable in ETCS.  The story: I've been looking at Colin McLarty's paper [A finite order arithemetic foundation for cohomology](http://arxiv.org/abs/1102.1773), which shows that nothing stronger than finite order arithmetic is needed anywhere in EGA or SGA.  I want to state that nothing stronger than ETCS is needed anywhere in EGA or SGA.  To back that up with references, I therefore need something that relates ETCS to finite order arithmetic.