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

[GeoffreySangston]

This one is also still open as of today, and looks like everything is set up to add it. I would do it but it's pretty far from the objects I normally study so I probably wouldn't do a good job.

π-Base, Search for metrizable + realcompact + ~Non-measurable cardinality