let M be Aleph; :: thesis: ( M is measurable implies M is limit_cardinal )

assume M is measurable ; :: thesis: M is limit_cardinal

then consider F being Filter of M such that

A1: F is_complete_with M and

A2: ( not F is principal & F is being_ultrafilter ) ;

assume A3: not M is limit_cardinal ; :: thesis: contradiction

F is_complete_with card M by A1;

hence contradiction by A2, A3, Th23, Th37; :: thesis: verum

assume M is measurable ; :: thesis: M is limit_cardinal

then consider F being Filter of M such that

A1: F is_complete_with M and

A2: ( not F is principal & F is being_ultrafilter ) ;

assume A3: not M is limit_cardinal ; :: thesis: contradiction

F is_complete_with card M by A1;

hence contradiction by A2, A3, Th23, Th37; :: thesis: verum