let M be non countable Aleph; :: thesis: ( M is strongly_Mahlo implies M is strongly_inaccessible )
assume M is strongly_Mahlo ; :: thesis: M is strongly_inaccessible
then ( M is strong_limit & M is regular ) by Th26, Th27, Th30;
hence M is strongly_inaccessible by CARD_FIL:def 15; :: thesis: verum