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

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