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 { N where N is infinite cardinal Element of M : N is strongly_inaccessible } is_stationary_in M by Def11;
then { N1 where N1 is infinite cardinal Element of M : N1 is regular } is_stationary_in M ;
hence M is Mahlo by Def10; :: thesis: verum