metrizable + realcompact => non-measurable cardinality

[Moniker1998]

Hi I'd like to replace theorem 394 by the stronger

P53 metrizable + P162 realcompact => P164 non-measurable

I don't think it exists in literature, here's the math stackexchange link for the proof

I've also asked for a better reference of this here

[Moniker1998]

I've got a response, K.P. Hart gave a very simple proof of this using Shirota's theorem
See here
I think this answer would be great for a reference. Shirota's theorem can be found in Gillman and Jerison