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 A2: cf M <> M by CARD_5:def 3;
cf M c= M by CARD_5:def 1;
then cf M in M by A2, CARD_1:3;
hence contradiction by A1, CARD_5:28; :: thesis: verum