I am just curious: is there a published proof of the compactness of the Hilbert cube that does not use the Axiom of Choice, or is it well known?