Least omega-measurable cardinal is measurable (source code)

= Least omega-measurable cardinal is measurable

If $\kappa$ is the least <omega-measurable cardinal> and $U$ witnesses it, failure of $\kappa$-completeness partitions a member of $U$ into fewer than $\kappa$ fibres, none belonging to $U$. The <pushforward ultrafilter> under the fibre-index map is then a nonprincipal countably complete measure on a smaller cardinal, a contradiction. Thus $U$ is $\kappa$-complete and $\kappa$ is a <measurable cardinal>.