let M be Aleph; :: thesis: ( M is strong_limit implies M is limit_cardinal )
assume A1: M is strong_limit ; :: thesis: M is limit_cardinal
assume not M is limit_cardinal ; :: thesis: contradiction
then consider N being Cardinal such that
A2: M = nextcard N by CARD_1:def 7;
M c= exp (2,N) by A2, Th24;
then A3: not exp (2,N) in M by CARD_1:14;
N in M by A2, CARD_1:32;
hence contradiction by A1, A3, Def14; :: thesis: verum