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 and
A4: not exp (2,N) in M ;
A5: nextcard N c= M by A3, CARD_3:90;
A6: N is infinite
proof
assume N is finite ; :: thesis: contradiction
then Funcs (N,2) is finite by FRAENKEL:6;
then card (Funcs (N,2)) is finite ;
then exp (2,N) is finite by CARD_2:def 3;
hence contradiction by A4, CARD_3:86; :: thesis: verum
end;
M c= exp (2,N) by A4, CARD_1:4;
then M c= nextcard N by A1, A6;
then nextcard N = M by A5;
hence contradiction by A2; :: thesis: verum