let M be Aleph; :: thesis: ( not M is limit_cardinal implies not M is countable )
assume A1: not M is limit_cardinal ; :: thesis: not M is countable
assume M is countable ; :: thesis: contradiction
then A2: card M c= omega by CARD_3:def 14;
card M = omega

proof

assume card M <> omega ; :: thesis: contradiction
then card M in omega by A2, CARD_1:3;
hence contradiction ; :: thesis: verum

end;

hence contradiction by A1; :: thesis: verum