let M be non countable Aleph; :: thesis: ( M is strongly_Mahlo implies M is Mahlo )
assume M is strongly_Mahlo ; :: thesis: M is Mahlo
then A2: { N where N is infinite cardinal Element of M : N is strongly_inaccessible } is_stationary_in M ;
A3: { N where N is infinite cardinal Element of M : N is strongly_inaccessible } c= { N1 where N1 is infinite cardinal Element of M : N1 is regular }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { N where N is infinite cardinal Element of M : N is strongly_inaccessible } or x in { N1 where N1 is infinite cardinal Element of M : N1 is regular } )
assume x in { N where N is infinite cardinal Element of M : N is strongly_inaccessible } ; :: thesis: x in { N1 where N1 is infinite cardinal Element of M : N1 is regular }
then consider N being infinite cardinal Element of M such that
B1: ( x = N & N is strongly_inaccessible ) ;
x in { N1 where N1 is infinite cardinal Element of M : N1 is regular } by B1;
hence x in { N1 where N1 is infinite cardinal Element of M : N1 is regular } ; :: thesis: verum
end;
{ N where N is infinite cardinal Element of M : N is regular } c= M
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { N where N is infinite cardinal Element of M : N is regular } or x in M )
assume x in { N where N is infinite cardinal Element of M : N is regular } ; :: thesis: x in M
then consider N being infinite cardinal Element of M such that
A1: ( x = N & N is regular ) ;
thus x in M by A1; :: thesis: verum
end;
then { N where N is infinite cardinal Element of M : N is regular } is_stationary_in M by A2, A3, Th14;
then M is Mahlo ;
hence M is Mahlo ; :: thesis: verum