:: deftheorem defines strongly_Mahlo CARD_LAR:def 11 :
for M being non countable Aleph holds
( M is strongly_Mahlo iff { N where N is infinite cardinal Element of M : N is strongly_inaccessible } is_stationary_in M );