let M be non countable Aleph; :: thesis: ( M is strongly_Mahlo implies M is strong_limit )
assume M is strongly_Mahlo ; :: thesis: M is strong_limit
then A1: { N where N is infinite cardinal Element of M : N is strongly_inaccessible } is_stationary_in M by Def11;
then reconsider SI = { N where N is infinite cardinal Element of M : N is strongly_inaccessible } as Subset of M by Def8;
assume not M is strong_limit ; :: thesis: contradiction
then consider M1 being Cardinal such that
A2: M1 in M and
A3: not exp 2,M1 in M by CARD_FIL:def 14;
succ M1 in M by A2, ORDINAL1:41;
then ( M \ (succ M1) is closed & M \ (succ M1) is unbounded ) by Th13;
then SI /\ (M \ (succ M1)) <> {} by A1, Def8;
then consider M2 being set such that
A4: M2 in SI /\ (M \ (succ M1)) by XBOOLE_0:def 1;
A5: ( M2 in SI & M2 in M \ (succ M1) ) by A4, XBOOLE_0:def 4;
then consider N being infinite cardinal Element of M such that
A6: N = M2 and
A7: N is strongly_inaccessible ;
( N in M & not N in succ M1 ) by A5, A6, XBOOLE_0:def 5;
then not N c= M1 by ORDINAL1:34;
then M1 in N by ORDINAL1:26;
then exp 2,M1 in N by A7, CARD_FIL:def 14;
hence contradiction by A3, ORDINAL1:19; :: thesis: verum