let M be Aleph; :: thesis: ( not M is limit_cardinal implies M is regular )
assume A1: not M is limit_cardinal ; :: thesis: M is regular
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 cf M in M by CARD_1:13;
hence contradiction by A1, CARD_5:40; :: thesis: verum