Yeah, that is not the axiom of choice and even if it were their conclusion is not correct. You can't characterize a set as non being described by finite symbols.

On the other hand, it's always refreshing to see someone pushing us to think in this constructs.

Logic is hard!