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 ;
M c= exp (2,N) by A2, Th24;
then A3: not exp (2,N) in M by CARD_1:4;
N in M by A2, CARD_1:18;
hence contradiction by A1, A3; :: thesis: verum