let M be Aleph; ( M is measurable implies M is regular )
A1:
cf M c= M
by CARD_5:def 1;
assume
M is measurable
; M is regular
then consider Uf being Filter of M such that
A2:
Uf is_complete_with M
and
A3:
( not Uf is principal & Uf is being_ultrafilter )
;
assume
not M is regular
; contradiction
then
cf M <> M
by CARD_5:def 3;
then A4:
cf M in M
by A1, CARD_1:3;
then consider xi being Ordinal-Sequence such that
A5:
dom xi = cf M
and
A6:
rng xi c= M
and
xi is increasing
and
A7:
M = sup xi
and
xi is Cardinal-Function
and
not 0 in rng xi
by CARD_5:29;
M = sup (rng xi)
by A7, ORDINAL2:def 5;
then A8:
M = union (rng xi)
by A6, Th32;
Uf is_complete_with card M
by A2;
then A9:
Uf is uniform
by A3, Th23;
A10:
rng xi c= dual Uf
card (rng xi) c= card (dom xi)
by CARD_2:61;
then
card (rng xi) c= cf M
by A5;
then A13:
card (rng xi) in M
by A4, ORDINAL1:12;
dual Uf is_complete_with M
by A2, Th12;
then
union (rng xi) in dual Uf
by A8, A13, A10, ZFMISC_1:2;
hence
contradiction
by A8, Def2; verum