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 ;
then reconsider SI = { N where N is infinite cardinal Element of M : N is strongly_inaccessible } as Subset of M ;
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:28;
then ( M \ (succ M1) is closed & M \ (succ M1) is unbounded ) by Th12;
then SI /\ (M \ (succ M1)) <> {} by A1;
then consider M2 being object such that
A4: M2 in SI /\ (M \ (succ M1)) by XBOOLE_0:def 1;
M2 in SI by A4, XBOOLE_0:def 4;
then consider N being infinite cardinal Element of M such that
A5: N = M2 and
A6: N is strongly_inaccessible ;
M2 in M \ (succ M1) by A4, XBOOLE_0:def 4;
then not N in succ M1 by A5, XBOOLE_0:def 5;
then not N c= M1 by ORDINAL1:22;
then M1 in N by ORDINAL1:16;
then exp (2,M1) in N by A6, CARD_FIL:def 14;
hence contradiction by A3, ORDINAL1:10; :: thesis: verum