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

then M c= nextcard N by A1, A6;

then nextcard N = M by A5;

hence contradiction by A2; :: thesis: verum

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

M c= exp (2,N)
by A4, CARD_1:4;
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;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

then M c= nextcard N by A1, A6;

then nextcard N = M by A5;

hence contradiction by A2; :: thesis: verum