let M be Aleph; :: thesis: ( GCH & M is limit_cardinal implies M is strong_limit )
assume A1: GCH ; :: thesis: ( not M is limit_cardinal or M is strong_limit )
assume A2: M is limit_cardinal ; :: thesis: M is strong_limit
assume not M is strong_limit ; :: thesis: contradiction
then consider N being Cardinal such that
A3: ( N in M & not exp 2,N in M ) by Def14;
A4: not N is finite

proof

assume N is finite ; :: thesis: contradiction
then Funcs N,2 is finite by FRAENKEL:16;
then card (Funcs N,2) is finite ;
then exp 2,N is finite by CARD_2:def 3;
hence contradiction by A3, CARD_3:103; :: thesis: verum

end;

M c= exp 2,N by A3, CARD_1:14;
then A5: M c= nextcard N by A1, A4, Def12;
nextcard N c= M by A3, CARD_3:107;
then nextcard N = M by A5, XBOOLE_0:def 10;
hence contradiction by A2, CARD_1:def 7; :: thesis: verum