let M be non countable Aleph; :: thesis: ( M is Mahlo implies M is limit_cardinal )
assume M is Mahlo ; :: thesis: M is limit_cardinal
then A1: { N where N is infinite cardinal Element of M : N is regular } is_stationary_in M ;
then reconsider REG = { N where N is infinite cardinal Element of M : N is regular } as Subset of M ;
assume not M is limit_cardinal ; :: thesis: contradiction
then consider M1 being Cardinal such that
A2: nextcard M1 = M by CARD_1:def 4;
M1 in M by A2, CARD_1:18;
then succ M1 in M by ORDINAL1:28;
then ( M \ (succ M1) is closed & M \ (succ M1) is unbounded ) by Th12;
then REG /\ (M \ (succ M1)) <> {} by A1;
then consider M2 being object such that
A3: M2 in REG /\ (M \ (succ M1)) by XBOOLE_0:def 1;
M2 in REG by A3, XBOOLE_0:def 4;
then consider N being infinite cardinal Element of M such that
A4: N = M2 and
N is regular ;
M2 in M \ (succ M1) by A3, XBOOLE_0:def 4;
then not N in succ M1 by A4, XBOOLE_0:def 5;
then not N c= M1 by ORDINAL1:22;
then M1 in N by ORDINAL1:16;
then ( N in M & nextcard M1 c= N ) by CARD_3:90;
then N in N by A2;
hence contradiction ; :: thesis: verum