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 }

then M is Mahlo ;

hence M is Mahlo ; :: thesis: verum

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

{ N where N is infinite cardinal Element of M : N is regular } c= M
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;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

proof

then
{ N where N is infinite cardinal Element of M : N is regular } is_stationary_in M
by A2, A3, Th14;
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;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

then M is Mahlo ;

hence M is Mahlo ; :: thesis: verum