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

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