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

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

hence
contradiction
by A1; :: thesis: verum
assume
card M <> omega
; :: thesis: contradiction

then card M in omega by A2, CARD_1:3;

hence contradiction ; :: thesis: verum

end;then card M in omega by A2, CARD_1:3;

hence contradiction ; :: thesis: verum