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