Has Grothendieck ever used expressions such as "Axiom of Choice", "Zermelo-Fraenkel", "proper class", etc?

In my humble opinion, Grothendieck's main motivation for introducing the Axiom of Universes was to make Category Theory Bourbaki compatible. Actually, this is implicit in Harry Gindi's statement of the question. Harry writes "this relative approach makes proper classes pointless". But from Bourbaki's perspective, the expression "proper class" just doesn't make sense. In short (in my interpretation of Grothendieck's thought) the function of this axiom was to make Category Theory soundly founded.

Dear Martin: You can take a look at Theorem 5.6.3 p. 305 in Algèbre et théories galoisiennes by Douady and Douady.

Dear Ian and dear T.: Thank you very much for your comments.

Same comment as above!

Now I understand. Very nice!

(My browser can't read your k!) I hesitated to give this argument. I told myself "the most naive way to attach a subset to a permutation is to form the set of fixed points" ...

Loomis's proof could be dubbed "Tychonoff's Theorem for dummies". That's why I like it!