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 Th27, Th28, Th31;
hence M is strongly_inaccessible by CARD_FIL:def 15; :: thesis: verum