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 ) by Def16;
A3: F is_complete_with card M by A1, CARD_1:def 5;
assume not M is limit_cardinal ; :: thesis: contradiction
hence contradiction by A1, A2, A3, Th23, Th37; :: thesis: verum