Mike is basically right about the AFA-vs-ZF distinction being irrelevant to "working mathematics." I feel the same about the IEEE floating point standard vis a vis various "good" NA algorithms I was exposed to long ago. But just now I was looking at an instance of Stone duality where I wanted to say of two partial lattices that each was the partial lattice of ultrafilters of the other. This is gibberish for ZF but not for AFA. The ZF expression of this requires me to stick in an "isomorphic to." AFA is not about doing something you couldn't do before, it is merely about not having to say you're sorry when you talk dirty. -v =============================