let M be Aleph; :: thesis: ( M is strongly_inaccessible implies M is inaccessible )
assume A1: M is strongly_inaccessible ; :: thesis: M is inaccessible
hence M is regular ; :: according to CARD_FIL:def 13 :: thesis: M is limit_cardinal
thus M is limit_cardinal by A1; :: thesis: verum