let M be Aleph; :: thesis: ( M is measurable implies M is regular )
assume M is measurable ; :: thesis: M is regular
then consider Uf being Filter of M such that
A1: Uf is_complete_with M and
A2: ( not Uf is principal & Uf is being_ultrafilter ) by Def16;
Uf is_complete_with card M by A1, CARD_1:def 5;
then A3: Uf is uniform by A2, Th23;
assume not M is regular ; :: thesis: contradiction
then ( cf M <> M & cf M c= M ) by CARD_5:def 2, CARD_5:def 4;
then A4: cf M in M by CARD_1:13;
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:41;
A8: M = sup (rng xi) by A7, ORDINAL2:def 9;
A9: M = union (rng xi) by A6, A8, Th32;
card (rng xi) c= card (dom xi) by CARD_2:80;
then card (rng xi) c= cf M by A5, CARD_1:def 5;
then A10: card (rng xi) in M by A4, ORDINAL1:22;
A11: rng xi c= dual Uf

proof

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

proof

assume X1 in Uf ; :: thesis: contradiction
then card X1 = card M by A3, Def5;
then card X1 = M by CARD_1:def 5;
hence contradiction by A13; :: thesis: verum

end;

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

end;

dual Uf is_complete_with M by A1, Th12;
then union (rng xi) in dual Uf by A9, A10, A11, Def4, ZFMISC_1:2;
hence contradiction by A9, Def2; :: thesis: verum