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

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