[codebje]

Perhaps this is an ignorant question, but wouldn't you need AC to select the s ⊆ A whose existence the contradiction depends on? A constructive proof, at least the ones I'm trying to build in my head, stumbles when needing to produce that s to use in the following arguments.

[SabrinaJewson]

No, because you only have to choose _one_ s for the proof to work, and a finite number of choices is valid in intuitionistic and constructive mathematics.