let M be Aleph; :: thesis: ( M is measurable implies M is regular )
A1: cf M c= M by CARD_5:def 1;
assume M is measurable ; :: thesis: 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 ; :: thesis: 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

proof

let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in rng xi or X in dual Uf )
assume A11: X in rng xi ; :: thesis: X in dual Uf
reconsider X1 = X as Subset of M by A6, A11, ORDINAL1:def 2;
A12: card X1 in M by A6, A11, CARD_1:9;
not X1 in Uf

proof

assume X1 in Uf ; :: thesis: contradiction
then card X1 = card M by A9;
then card X1 = M ;
hence contradiction by A12; :: thesis: verum

end;

hence X in dual Uf by A3, Th22; :: thesis: verum

end;

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; :: thesis: verum