let a be Aleph; :: thesis: ( cf a in a implies a is limit_cardinal )
assume A1: cf a in a ; :: thesis: a is limit_cardinal
given M being Cardinal such that A2: a = nextcard M ; :: according to CARD_1:def 4 :: thesis: contradiction
cf a c= M by A1, A2, CARD_3:91;
then reconsider M = M as Aleph ;
nextcard M in nextcard M by A1, A2, Th22;
hence contradiction ; :: thesis: verum